论文部分内容阅读
传统的模型精化过程中模型间一致性检测专注于检测模型自身的正确性、死锁、以及不变式保持性等,而无法保证模型间行为方面的一致性。为此提出利用系统行为属性来反应模型行为,结合模型检测的方法来检测模型间的行为一致性。首先对精化前模型分析生成抽象测试用例并抽取其代表的系统行为属性;然后根据精化后的模型抽取模型精化关系并进一步更新系统属性;最后使用这些系统行为属性来验证精化后的模型是否依然满足其代表的系统行为,如果不满足则说明模型间存在不一致行为,可以通过生成的反例路径找出不一致的位置。实验结果表明使用该方法可