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.
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: 12 Mar 2019 *