本发明公开了一种面向NuXMV的安全关键系统状态转换图测试用例生成方法，S1，将变量关系模型转换为NuXMV符号模型检查器可接受的状态转换图模型，根据状态转换图可解释化预处理算法，读取和解析所述图模型文件，对图模型进行预处理，从状态转换图模型中解析出结点流和条件流；S2，对解析出的结点流和条件流进行规约，制定不同的覆盖策略，并基于覆盖策略通过验证存在性属性的方式生成反例状态转移路径，存入测试用例集中；S3，对S2得到的测试用例集去冗余化，得到最小最优的测试用例集。本发明能够找出安全关键系统在编码过程中存在的安全性问题，验证编码和设计的一致性，提高安全关键系统的可靠性。