基于带参系统Murphi模型的SMV自动建模

Automatic Modeling in SMV Based on Murphi Model of Parameterized Systems

提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建模比较容易,而且得到的模型代码量比较少,易于阅读、理解和修改;而SMV模型则能实现更丰富的控制,如进行快速不变式检查和限界模型检测等,但是建模过程复杂,模型不易维护.我们通过对两者进行分析,首先提出了能够很好描述带参系统的一个语义模型,然后读入相应的Murphi模型并进行分析以获取其语义模型表示,最后再通过一系列的策略自动得到限定参数时的SMV模型,由此得到的模型能够满足实际科研工作的应用要求.

We present a method for automatic modeling in SMV of a parameterized system based on its corresponding Murphi Model. Modeling in Murphi for parameterized systems is easy because its parameterization feature, and a Murphi model code is relatively small and is not very complex to read, understand and modify. On the other hand, an SMV model could give more powerful operations, such as quick invariant checking and bounded model checking, but it is very hard to model in SMV for a parameterized system and to maintain an SMV model. We present a semantic model which is well able to describe a parameterized system, then analyze a Murphi model to create its semantic model, finally we get its corresponding SMV model which is effective for research work automatically by a series of conversion strategies.