模型检验在构件数据流测试中的应用

摘要：

模型检验输出的反例提供了一种自动产生测试用例的有效途径.提出了一种用模型检验进行构件数据流测试的方法.利用构件状态机描述构件的外部行为,用带有变量定义和使用标记的Kipke结构描述构件状态迁移中的数据流信息;给出了从构件状态机到Kripke结构的转换方法,并建立了全定义覆盖和全使用覆盖准则的陷阱性质构造公式.陷阱性质将使模型检验器NuSMV输出反例,从而产生构件的数据流测试序列.

关键词：构件、数据流测试、模型检验、陷阱性质

所属期刊栏目：4

分类号：TP311(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.60970007, 61073050;the Natural Science Foundation of Shanghai of China under Grant No.09ZR1412100;the Science and Technology Commission Project of Shanghai of China under Grant No.10510704900;the Shanghai Leading Academic Discipline Project of China under Grant No.J50103

在线出版日期：2011-03-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1121-1130