Title :
UML_AD2EventB: An Approach to Generating Event B Specification from UML Activity Diagrams for the Workflows Specification and Verification
Author :
Ben Younes, Ahlem ; Ayed, L.
Author_Institution :
Res. Unit of Technol. of Inf. & Commun. (UTIC), ESSTT, Tunisia
Abstract :
In this paper, we present a new approach to generating Event B specification from UML Activity Diagrams (AD). The goal of this work is to define a formal semantics of activity diagrams that is suitable for workflows modelling. The semantics should allow verification of functional requirements using the B powerful support tools like B4free. In important characteristic of workflows is that the workflow systems are reactive systems. In this paper, we present a formal syntax and semantic for UML AD endowed with interactive aspects (send/receive event concepts), and we illustrate the proposed technique by an example of workflow application.
Keywords :
Unified Modeling Language; formal specification; formal verification; B4free; Event B specification generation; UML activity diagrams; formal semantics; reactive systems; workflow application; workflows modelling; Application software; Explosions; Formal verification; Large-scale systems; Power system modeling; Refining; Space technology; State-space methods; System recovery; Unified modeling language; Event B; Formal verification; Specification; UML; Validation; workflow application;
Conference_Titel :
Services - I, 2009 World Conference on
Conference_Location :
Los Angeles, CA
Print_ISBN :
978-0-7695-3708-5
Electronic_ISBN :
978-0-7695-3708-5
DOI :
10.1109/SERVICES-I.2009.101
