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

作者：马占有; 郭昊; 李召恺; 李健祥

来源：华中科技大学学报(自然科学版)科技大学, 2023, 1-6.

DOI：10.13245/j.hust.240212

• 模型检测
• 统一建模语言
• 模型转换
• 计算树逻辑
• 符号模型检测器

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

• 单位
  北方民族大学