Formal Semantics of UML State Machine Diagrams with Concurrent Behaviors
In software development,UML(Unified Modelling Language)state machine diagrams are one of the most popular forms of modelling,which are semi-formal models and cannot be reasoned about in a formal way.In order to be able to reason about UML state machine diagrams,existing work uses Petri nets,temporal logic language XYZ/E,dynamic description logic,Z(Object-Z)language,CHAM chemical abstraction machine,etc.as the formal semantics of the state machine diagrams,but these semantics are behavioural se-mantics,and there is no formal semantics embodying the true concurrency directly from the structure.We propose a new model,the Unified Structural Model,as the formal semantics of UML state machine diagrams with concurrency behaviours,which does not add or subtract any information from the state machine diagrams.Based on the Unified Structural Model,firstly,the configuration(global state)of a state machine diagram is defined,which is used to represent the execution process of a state machine diagram,and the transformation rules of the configuration of a UML state machine diagram are given to illustrate how the configuration is executed in a state machine dia-gram,based on which the accessibility algorithms of state machine diagrams are given.Then properties such as deadlocks of state machine diagrams are also introduced.Finally,a prototype tool is developed that implements the accessibility analysis of state machine di-agrams,and the application of the methodology is illustrated with examples.
国家科技期刊平台
NSTL
万方数据
