https://jjcit.org/paper/111
INTEGRATING UML 2.0 ACTIVITY DIAGRAMS AND PI-CALCULUS FOR MODELING AND VERIFICATION OF SOFTWARE SYSTEMS USING TGG
10.5455/jjcit.71-1587215553
Raida Elmansouri,Said Meghzili,Allaoua Chaoui,Aissam Belghiat,Omar Hedjazi
Model-driven engineering,TGG,Xpand,UML activity diagrams,Pi-calculus,Model transformation,Graph transformation,Software systems
1
2480
962
18-Apr.-2020
18-Jun.-2020 and 26-Jul.-2020
24-Aug.-2020
This paper deals with modeling and verification of software systems by combining UML diagrams and Pi-
calculus. UML 2.0 Activity diagrams are used for modeling the behavior of software systems, while Pi-calculus
is used for semantic and verification purposes. More precisely, UML is a semi-formal language and so it needs
formal semantics for its constructs and lacks tools for verifying properties. To this end, we propose an approach
and a tool called AD2PICALC for transforming UML 2.0 Activity diagrams to Pi-calculus processes using
Eclipse Xpand and TGG tools. The obtained Pi-calculus processes are then used as input for Pi-calculus tools,
like MWB, to verify some properties as deadlocks, safety, determinism, termination and livelock. We illustrate
our contribution through an example from the literature and verify the property of deadlock using MWB tool.
The main contribution of this paper lies in the automation of the transformation approach using TGG tools.