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

Modeling and verification of concurrent system based on UML-NuSMV

作　　者：马占有[1] 郭昊 李召恺 李健祥 MA Zhanyou;GUO Hao;LI Zhaokai;LI Jianxiang(School of Computer Science and Engineering,North Minzu University,Yinchuan 750030,China)

机构地区：[1]北方民族大学计算机科学与工程学院,宁夏银川750030

出　　处：《华中科技大学学报（自然科学版）》2024年第2期90-95,共6页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(61962001);宁夏自然科学基金资助项目(2021AAC03004).

摘　　要：为解决直接建立系统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.

关 键 词：模型检测 统一建模语言 模型转换 并发系统 符号模型检测器 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]