摘要:
摘要: 安全关键系统必须满足规定的安全性质. 测试生成通常独立于给定性质,“先验证再测试”的方法不能保证安全性质被测试. 为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法. 用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例. 给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法. 使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.
中图分类号:
曾红卫1, 缪淮扣1;2. 用模型检验产生安全性质的测试[J]. 应用科学学报, 2011, 29(5): 529-536.
ZENG Hong-wei1, MIAO Huai-kou1;2. Generate Safety Property Tests Using Model Checking[J]. Journal of Applied Sciences, 2011, 29(5): 529-536.