论文部分内容阅读
安全关键系统必须满足规定的安全性质．测试生成通常独立于给定性质，“先验证再测试”的方法不能保证安全性质被测试．为此，该文提出了一种基于输入一输出标记迁移系统的安全性质测试方法．用输出变异建立被测实现的输出一完全模型，通过发现危险迹产生测试用例．给出了基于图结构覆盖的安全性质测试准则，提出了形式化测试准则的方法．使用模型检验器NuSMV检验输出一完全模型可产生既满足结构覆盖又与安全性质相关的测试用例．