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

Model checking UML Statechart based on Spin

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.