版权所有：内蒙古大学图书馆 技术提供：维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
用模型检验产生安全性质的测试
Generate Safety Property Tests Using Model Checking作者机构：上海大学计算机工程与科学学院上海200072 上海市计算机软件评测重点实验室上海201112
出 版 物：《应用科学学报》 (Journal of Applied Sciences)
年 卷 期：2011年第29卷第5期
页 面：529-536页
核心收录：
学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金(No.60970007 No.61073050) 上海市自然科学基金(No.09ZR1412100) 上海市科学技术委员会项目基金(No.10510704900) 上海市重点学科建设项目基金(No.J50103)资助
摘 要：安全关键系统必须满足规定的安全性质.测试生成通常独立于给定性质,先验证再测试的方法不能保证安全性质被测试.为此,该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法.用输出变异建立被测实现的输出-完全模型,通过发现危险迹产生测试用例.给出了基于图结构覆盖的安全性质测试准则,提出了形式化测试准则的方法.使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.
