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

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

Refinement Checking Based on Simulation Relations

Refinement checking is an important method in formal verification, which shows 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. In order to verify different kinds of properties, traces, stables failures and failures/divergence refinement checking have been proposed. Refinement checking often relies on the subset construction, and 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 ones significantly, and can be directly used in traces refinement checking. On this basis, this work further proposes stable failures and failures-divergence refinement checking algorithms based on simulation relations. On the other hand, 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 show the efficiency of our approaches.