基于模拟关系的精化检测方法

来源：软件学报杂志2016年第3期北京时间：

作者：王婷,陈铁明,刘杨

单位：王婷，浙江工业大学计算机科学与技术学院, 浙江 杭州 31002311,陈铁明，浙江工业大学计算机科学与技术学院, 浙江 杭州 31002302,刘杨，School of Computer Engineering, Nanyang Technological University, Singapore 639798, Singapore03

摘要：精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.

关键词：精化检测;模拟;failures;divergence;时间自动机

基金资助：国家自然科学基金(61103044,U1509214);浙江省自然科学基金(LQ15E050006,LY16F020035)