Towards a Formal Semantic for UML 2.0 Activity Diagram based on Institution Theory

摘要

In the present paper, we aim to extend the institution of UML Activity Diagram, which is defined in our previous work. In fact, the syntax definition will be more enriched throw taking into account the different syntax dependencies between Activity nodes in UML Activity Diagram models. As for institution theory, it proves its adequacy to cope with such theoretic foundation. As a result, we define a formal semantic of UML 2.0 AD relating the syntax and the semantic under the satisfaction condition. Thus, we further advance the approach by laying a solid theoretical foundation via formally defining the semantics and the syntax of UML Activity Diagram notation. Then, we prove that UML Activity Diagram syntax definitions and their induced formal logic form an institution of formal specification for modelling.