Institution-based UML activity diagram transformation with semantic preservation
by Amine Achouri; Yousra Bendaly Hlaoui; Leila Jemni Ben Ayed
International Journal of Computational Science and Engineering (IJCSE), Vol. 18, No. 3, 2019

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.

Online publication date: Tue, 26-Mar-2019

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computational Science and Engineering (IJCSE):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com