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