%0 Journal Article
%T 基于模拟关系的精化检测方法
%A 刘杨
%A 王婷
%A 陈铁明
%J -
%D 2016
%R 10.13328/j.cnki.jos.004982
%X 精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高
%K 精化检测 模拟 failures divergence 时间自动机
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=4982&flag=1