Article: Institution-based UML activity diagram transformation with semantic preservation Journal: International Journal of Computational Science and Engineering (IJCSE) 2019 Vol.18 No.3 pp.240 - 251 Abstract: This paper presents a specific tool, called MAV-UML-AD, allowing the specification and the verification of workflow models using UML activity diagrams (UML ADs) and Event-B and based on institutions. The developed tool translates an activity diagram model into an equivalent Event-B specification according to a mathematical semantics. The transformation approach of UML AD models is based on the theory of institutions. In fact, each of UML AD and Event-B specifications is defined by an instance of its corresponding institution. The transformation approach is represented by an institution co-morphism which is defined between the two institutions. Institution theory is adopted as the theoretical framework of the tool essentially for two reasons. First, it gives a locally mathematical semantics for UML AD and Event-B. Second, it defines a semantic preserving mapping between UML AD specification and Event-B machine. Thanks to the B theorem prover, functional proprieties like liveness and fairness can be formally checked. The core of the model transformation approach will be highlighted in this paper and how institution concepts such as category, co-morphism and signature are presented in the two used formalisms. This paper will also illustrate the use of the developed tool MAV-UML-AD through an example of specification and verification. Inderscience Publishers - linking academia, business and industry through research

Title: Institution-based UML activity diagram transformation with semantic preservation

Authors: Amine Achouri; Yousra Bendaly Hlaoui; Leila Jemni Ben Ayed

Addresses: Laboratory LaTICE – ESSTT, University of Tunis, Tunisia ' Laboratory LaTICE – ESSTT, University of Tunis, Tunisia ' Laboratory LaTICE – ESSTT, University of Tunis, Tunisia

Abstract: This paper presents a specific tool, called MAV-UML-AD, allowing the specification and the verification of workflow models using UML activity diagrams (UML ADs) and Event-B and based on institutions. The developed tool translates an activity diagram model into an equivalent Event-B specification according to a mathematical semantics. The transformation approach of UML AD models is based on the theory of institutions. In fact, each of UML AD and Event-B specifications is defined by an instance of its corresponding institution. The transformation approach is represented by an institution co-morphism which is defined between the two institutions. Institution theory is adopted as the theoretical framework of the tool essentially for two reasons. First, it gives a locally mathematical semantics for UML AD and Event-B. Second, it defines a semantic preserving mapping between UML AD specification and Event-B machine. Thanks to the B theorem prover, functional proprieties like liveness and fairness can be formally checked. The core of the model transformation approach will be highlighted in this paper and how institution concepts such as category, co-morphism and signature are presented in the two used formalisms. This paper will also illustrate the use of the developed tool MAV-UML-AD through an example of specification and verification.

Keywords: formal semantics; institution; model driven engineering; Event-B; UML activity diagram; UML AD; formal verification.

DOI: 10.1504/IJCSE.2019.098534

International Journal of Computational Science and Engineering, 2019 Vol.18 No.3, pp.240 - 251

Received: 03 Mar 2016
Accepted: 28 Aug 2016
Published online: 26 Mar 2019 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article

Title: Institution-based UML activity diagram transformation with semantic preservation

Keep up-to-date