基于Spin的UML状态图模型检查的设计与实现

计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (10): 43-47.

基于Spin的UML状态图模型检查的设计与实现

郭伟¹,缪力¹,张大方^1,2,闵应骅³

1.湖南大学软件学院，长沙 410082
2.湖南大学计算机与通信学院，长沙 410082
3.中国科学院计算技术研究所，北京 100080

收稿日期:2007-07-20 修回日期:2007-09-24 出版日期:2008-04-01 发布日期:2008-04-01
通讯作者: 郭伟

Model checking UML Statechart based on Spin

GUO Wei¹,MIAO Li¹,ZHANG Da-fang^1,2,MIN Ying-hua³

1.Software College，Hunan University，Changsha 410082，China
2.College of Computer and Communication，Hunan University，Changsha 410082，China
3.Institute of Computer Technology，Chinese Academy of Sciences，Beijing 100080，China

Received:2007-07-20 Revised:2007-09-24 Online:2008-04-01 Published:2008-04-01
Contact: GUO Wei

摘要/Abstract

摘要： UML已经是软件建模方面的标准语言，UML Statechart描述了系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高，Statechart往往包含设计者所未预料到的隐患，通过模型检查来对Statechart进行穷举检验就成为一个重要课题，首先给出了含层次、并发Statechart的语义；随后提出了对Statechart进行模型检查的一种新方法，并且已经编写软件SC2Spin实现此方法，该方法使用了提出的Statechart山脉算法和迁移提取法，可以将一个Statechart自动转化为Spin的输入语言Promela，从而验证Statechart的死锁、活锁等错误和时序逻辑公式。

关键词: 模型检查, Statechart, Statechart山脉算法, 迁移提取, Spin

Abstract: Being an industry standard of software modeling language，UML is well accepted and extensively used in the industry.The UML Statechart describes some dynamic behavior of a system in its lifecycle.With systems to be modeled using Statechart become more and more large and complex，the Statechart often contain unexpected hidden dangers.It is then necessary to check the consistency and correctness.The paper presents an approach to model checking UML Statechart containing hierarchy and concurrent states.The software named SC2Spin is completed to check Statechart automatically.First semantics of Statechart is defined and then a new method to check Statechart is proposed，the Statechart is translated to Promela which is the input language of the famous model checking tool SPIN.To implement this method，this paper proposes Statechart Mountain Algorithm（SMA） to analyze the Translation in Statechart，proposes Translation Extraction to implement the translation.SC2Spin can detect errors like Deadlocks and Livelocks and verify LTL formulas.

Key words: model checking, Statechart, Statechart Mountain Algorithm（SMA）, Transition Extraction, Spin

郭伟¹,缪力¹,张大方^1,2,闵应骅³. 基于Spin的UML状态图模型检查的设计与实现[J]. 计算机工程与应用, 2008, 44(10): 43-47.

GUO Wei¹,MIAO Li¹,ZHANG Da-fang^1,2,MIN Ying-hua³. Model checking UML Statechart based on Spin[J]. Computer Engineering and Applications, 2008, 44(10): 43-47.

[1]	杜梦瑶，王峥，李娜，强彦. 适用于无线体域网的动态口令认证协议[J]. 计算机工程与应用, 2020, 56(14): 68-73.
[2]	杨文霞，王峥，李娜，马建芬. 轻量级移动支付协议LMPP的安全性分析与改进[J]. 计算机工程与应用, 2019, 55(16): 88-93.
[3]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[4]	潘文林. 对象角色模型局部语义冲突即时检查方法研究[J]. 计算机工程与应用, 2015, 51(18): 144-150.
[5]	尤启房，杨晋吉. SIP协议的SPIN模型检测[J]. 计算机工程与应用, 2014, 50(13): 87-89.
[6]	吕威，黄志球，陈哲，阚双龙，魏欧. ESpin*：基于SPIN的Eclipse模型检测环境[J]. 计算机工程与应用, 2013, 49(7): 45-51.
[7]	缪力，谭志华，张大方. 基于SPIN的网络认证协议高效模型检测[J]. 计算机工程与应用, 2012, 48(21): 62-67.
[8]	杨爱萍,王成优,何凯. 简单有效的小波域图像插值放大算法[J]. 计算机工程与应用, 2009, 45(4): 9-10.
[9]	谭亮,曾红卫. 基于接口自动机的Web应用验证[J]. 计算机工程与应用, 2009, 45(3): 70-73.
[10]	陆公正¹，吴澜波₂，张广泉³. 定义及验证UML Statechart图中的数据流语义[J]. 计算机工程与应用, 2009, 45(24): 56-59.
[11]	吴昌,肖美华. 基于SPIN的IKEv2协议高效模型检测[J]. 计算机工程与应用, 2008, 44(5): 158-161.
[12]	张君昌,周瑾,何明一. 融合分形小波图像去噪和插值的新算法[J]. 计算机工程与应用, 2008, 44(30): 175-177.
[13]	缪力,张大方. 通信下推系统的一种有界可达算法[J]. 计算机工程与应用, 2008, 44(24): 19-21.
[14]	陈超,李俊,孔德光,帅建梅. 模型检测迷惑二进制恶意代码[J]. 计算机工程与应用, 2008, 44(15): 61-64.
[15]	周瑾,张君昌,何明一. 一种基于DCT Cycle Spinning的图像压缩方法[J]. 计算机工程与应用, 2008, 44(10): 157-159.