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

• 作者: 刘杨 王婷 陈铁明
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 精化检测 模拟 failures divergence 时间自动机
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件形式化方法与应用专题
• 页码范围: 580-592
• 页数: 13页
• 分类号: TP301
• 字数: 12820字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004982

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈铁明	浙江工业大学计算机科学与技术学院	60	357	11.0	15.0
2	王婷	浙江工业大学计算机科学与技术学院	13	11	3.0	3.0