基于模型检验的构件数据流测试

摘要：

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

关键词： 数据流测试 模型检验 陷阱性质 构件状态机 覆盖准则

作者: 曾红卫 缪淮扣

作者单位: 上海大学 计算机工程与科学学院,上海 200072

会议类型: 国内会议

会议名称: 2009中国计算机大会

会议地点: 天津

会议语种:中文

页码: 568-575

在线出版日期: 2009-10-23（万方平台首次上网日期，不代表论文的发表时间）