An Operational Semantics for UML Activity Diagrams

More and more large systems are taking UML (unified model language) as requirements description language for system analysis and design, especially in those safety-critical systems. One of the most important dynamic behaviors specifying the mechanism of UML is the UML activity diagram, which is widely used for modeling of business. The UML activity diagram lacks strictly defined formal dynamic semantics. It is difficult using the UML activity diagram to make formal analysis, verification and assertation. An operational semantics for UML activity diagram is proposed according to UML1.5 specification documents. First, the formal syntax of UML activity diagram is provided. Then, the configuration and the transitions are defined in detail. Finally, the deduct rules of UML activity diagram are described based on the LTS. The main contributions are: Firstly, in order to get more precise and clearer description of formal semantics, the hierarchy of activity state is abandoned and instead the concept of state bag is introduced to define the configuration. Secondly, the LTS semantics and the detailed deduction rules of UML activity diagram are defined. The global state transition diagram can be computed from the LTS semantics conveniently. Therefore, the formal semantics is able to deal with most of the features of UML activity diagram and can be used in formal verification.