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

Model checking UML Statechart based on Spin

作　　者：郭伟[1] 缪力[1] 张大方[1] 闵应骅[2] 

机构地区：[1]湖南大学软件学院,长沙410082 [2]中国科学院计算技术研究所,北京100080

出　　处：《计算机工程与应用》2008年第10期43-47,共5页Computer Engineering and Applications

基　　金：国家部委基础科研“十一五”项目;国家自然科学基金(the National Natural Science Foundation of China under Grant No.60673155)

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

关 键 词：模型检查 STATECHART Statechart山脉算法 迁移提取 SPIN 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]