基于UML-NuSMV的并发系统建模与验证

Modeling and verification of concurrent system based on UML-NuSMV

为解决直接建立系统NuSMV(符号模型检测器)模型的困难,提出一种从UML(统一建模语言)模型转换到NuSMV模型的方法,实现了UML与NuSMV结合的形式化验证.首先,使用UML中的视图对系统进行描述,建立系统的UML模型;然后,设计转换规则并给出转换算法,实现从UML模型到NuSMV模型的自动转换;最后,使用计算树逻辑对系统的属性进行描述,并通过NuSMV完成对系统的形式化验证.以一个双按键并发电梯系统为例,说明了基于UML-NuSMV的并发系统建模与验证过程.

To solve the difficulty of directly establishing a system NuSMV(symbolic model checker)model,a method was proposed to transform from UML(unified modeling language)model to NuSMV model,achieving formal verification of the combination of UML and NuSMV.Firstly,the system was described by using the vision of UML and the UML model of the system was established.Secondly,the conversion rules were designed and conversion algorithms were provided to achieve automatic conversion from UML models to NuSMV models.Thirdly,the properties of the system were described using computational tree logic and the formal verification of the system was completed through NuSMV.Finally,an example of a double-button concurrent elevator system was proposed to illustrate the modeling and verification process of concurrent system based on UML-NuSMV.