华中科技大学学报（自然科学版）2024，Vol.52Issue(2)：90-95,6.DOI:10.13245/j.hust.240212
基于UML-NuSMV的并发系统建模与验证
Modeling and verification of concurrent system based on UML-NuSMV
摘要
Abstract
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.关键词
模型检测/统一建模语言/模型转换/并发系统/符号模型检测器Key words
model checking/unified modeling language/model conversion/concurrent system/symbolic model checker分类
信息技术与安全科学引用本文复制引用
马占有,郭昊,李召恺,李健祥..基于UML-NuSMV的并发系统建模与验证[J].华中科技大学学报（自然科学版）,2024,52(2):90-95,6.基金项目
国家自然科学基金资助项目(61962001) （61962001）
宁夏自然科学基金资助项目(2021AAC03004). （2021AAC03004）
