This paper deals with modeling and verification of software systems by combing UML diagrams and Pi-calculus. UML 2.0 Activity diagrams are used for modeling the behavior of software systems while the 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 for 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 consists in the automation of the transformation approach using TGG tools.
Key words: Model-Driven Engineering, TGG, Xpand, UML activity diagrams, Pi-calculus, Model Transformation, Graph Transformation, Software Systems.
|
