Model checking UML Statechart based on Spin
Yinghua Min · Computer Engineering and Applications Journal · 2008
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.