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

Refinement Checking Based on Simulation Relations

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

Refinement checking is an important method in formal verification to convey a refinement relationship between an implementation model and a specification model in the same language. If the specification satisfies certain property and the refinement relationship is strong enough to preserve the property, then implementation satisfies the property. Refinement checking was developed in order to verify different kinds of properties, traces, stables failures and failures/divergence. Refinement checking often relies on the subset construction, thus suffers from state space explosion. Recently, some researchers proposed a simulation based approach for solving the language inclusion problem of NFA, which outperforms the previous methods significantly and can be directly used in traces refinement checking. Base on this advancement, this work further proposes stable failures and failures-divergence refinement checking algorithms based on simulation relations. In addition, this work also extends the idea of trace refinement checking to timed systems, and proposes timed automata traces refinement checking based on simulation relations. Experimental results confirm the efficiency of the presented approaches.