INTEGRATING UML 2.0 ACTIVITY DIAGRAMS AND PI-CALCULUS FOR MODELING AND VERIFICATION OF SOFTWARE SYSTEMS USING TGG

(Received: 18-Apr.-2020, Revised: 18-Jun.-2020 and 26-Jul.-2020 , Accepted: 24-Aug.-2020)

Authors Raida Elmansouri, Said Meghzili, Allaoua Chaoui, Aissam Belghiat, Omar Hedjazi,

Keywords #Model-driven engineering #TGG #Xpand #UML activity diagrams #Pi-calculus #Model transformation #Graph transformation #Software systems

Abstract 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.

References

[1] M. Singh, A. K. Sharma and R. Saxena, "An UML+ Z Framework for Validating and Verifying the Static Aspect of Safety Critical System," Procedia-Computer Science, vol. 85, pp. 352-361, 2016.

[2] R. M. Borges and A. C. Mota, "Integrating UML and Formal Methods," Electronic Notes in Theoretical Computer Science, vol. 184, pp. 97-112, 2007.

[3] OMG UML, [Online], Available: http://www.omg.org/spec/UML/2.2/Superstructure.

[4] F. R. Golra, F. Dagnat, J. Souquières, I. Sayar and S. Guerin, "Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation," Proc. of the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), pp. 54-69, Toulouse, France, Jun. 2018.

[5] R. Milner, Communicating and Mobile Systems: The Pi Calculus, Cambridge University Press, 1999.

[6] J. Parrow, "An Introduction to the Pi-calculus," Chapter to Appear in Handbook of Process Algebra, Ed. Bergstra, Ponse and Smolka, Elsevier, [Online], Available: http://courses.cs.vt.edu/cs5204/fall09- kafura/Papers/PICalculus/Pi-calculus-Introduction.pdf.

[7] A. R. Da Silva, "Model-driven Engineering: A Survey Supported by the Unified Conceptual Model," Computer Languages, Systems & Structures, vol. 43, pp. 139-155, 2015.

[8] S. Efftinge, P. Friese, A. Hase, D. Hübner, C. Kadura, B. Kolb et al., "Xpand Documentation," Technical Report, Copyright 2004-2010, [Online], Available: https://git.eclipse.org/c/m2t/org.eclipse. xpand.git/plain/doc/org.eclipse.xpand.doc/manual/xpand_reference.pdf, 2004.

[9] TGG Home Page, [Online], Available: www.informatik.uni-marburg.de/~swtagtive-contest/.

[10] B. Victor and F. Moller, "The Mobility Workbench—A Tool for the π-calculus," Proc. of the International Conference on Computer Aided Verification, pp. 428-440, Springer, Berlin, Heidelberg, 1994.

[11] R. Milner, "A Calculus of Communicating Systems," Lecture Notes in Computer Science, vol. 92, 1980.

[12] É. André, C. Choppy and G. Reggio, "Activity Diagram Patterns for Modeling Business Processes," Software Engineering Research, Management and Applications, Part of Studies in Computational Intelligence, vol. 496, pp. 197-213, Springer, Heidelberg, 2014.

[13] B. Hazela, D. Arora and V. Saxena, "Formalizing Semantics for UML Activity Diagram through Regular Expression Translation," Research Journal of Applied Sciences, Engineering and Technology, vol. 11, no. 2, pp 169-175, 2015.

[14] Y. Rahmoune, A. Chaoui and E. Kerkouche, "A Framework for Modeling and Analysis of UML Activity Diagram Using Graph Transformation," Procedia-Computer Science, vol. 56, pp. 612-617, 2015.

[15] M. Jamal and N. A. Zafar, "Transformation of Activity Diagrams into Colored Petri Nets Using Weighted Directed Graph," Proc. of the IEEE International Conference on Frontiers of Information Technology (FIT), pp. 181-186, Islamabad, Pakistan, December 2016.

[16] I. Chishti, A. Basukoski, T. Chaussalet and N. Beeknoo, "Transformation of UML Activity Diagram for Enhanced Reasoning," Proceedings of the Future Technologies Conference, pp. 466-482, Springer, Cham, 2018.

[17] A. Achouri, Y. B. Hlaoui and L. J. B. Ayed, "Institution-based UML Activity Diagram Transformation with Semantic Preservation," International Journal of Computational Science and Engineering, vol. 18, no. 3, pp. 240-251, 2019.

[18] L. B. R. dos Santos, V. A. de Santiago Junior and N. L. Vijaykumar, "Transformation of UML Behavioral Diagrams to Support Software Model Checking," Proc. of Formal Engineering Approachesto Software Components and Architectures (FESCA), vol. 147, pp. 133–142, doi:10.4204/EPTCS.147.10, 2014.

[19] NuSMV Home Page, "NuSMV: A New Symbolic Model Checker," [Online], Available: http://nusmv.fbk.eu/.

[20] S. Meghzili, A. Chaoui, M. Strecker and E. Kerkouche, "On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL," Proc. of IEEE International Conference on Information Reuse and Integration (IRI), pp. 419-426, San Diego, CA, USA, 2017.

[21] S. Meghzili, A. Chaoui, M. Strecker and E. Kerkouche, "Verification of Model Transformations Using Isabelle/HOL and Scala," Information Systems Frontiers, vol. 21, no. 1, pp. 45-65, 2019.

[22] K. Pokozy-Korenblat and C. Priami, "Toward Extracting π-calculus from UML Sequence and State Diagrams," Electronic Notes in Theoretical Computer Science, vol. 101, pp. 51-72, 2004.

[23] A. Belghiat and A. Chaoui, "A TGG Approach for Bidirectional Automatic Mapping between UML and Pi-calculus," Proceedings of the International Conference on Intelligent Information Processing, Security and Advanced Communication, Article no. 70, pp. 1-3, [Online], Available: https://doi.org/10.1145/2816839.2816857, ACM, 2015.

[24] A. Belghiat, A. Chaoui and M. Beldjehem, "Capturing and Verifying Dynamic Program Behaviour Using UML Communication Diagrams and Pi-calculus," Proc. of IEEE International Conference on Information Reuse and Integration, pp. 318-325, San Francisco, CA, USA, 2015.

[25] A. Belghiat and A. Chaoui, "A Graph Transformation of Activity Diagrams into π-calculus for Verification Purpose," Proceedings of the 3rd Edition of the International Conference on Advanced Aspects of Software Engineering (ICAASE18), pp. 107-114, Constantine, Algeria, Dec. 2018.

[26] MSDL, "AToM3 Quick Links," [Online], Available: http://atom3.cs.mcgill.ca/.

[27] V. S. Lam, "On π-calculus Semantics As a Formal Basis for UML Activity Diagrams," International Journal of Software Engineering and Knowledge Engineering, vol. 18, no. 4, pp. 541-567, 2008.

[28] A. Schürr, "Specification of Graph Translators with Triple Graph Grammars," Proc. of the International Workshop on Graph-Theoretic Concepts in Computer Science, Lecture Notes in Computer Science, vol. 903, pp. 151-163, Springer, Berlin, Heidelberg, 1994.

[29] A. Königs, "Model Transformation with Triple Graph Grammars," Proc. of Model Transformations in Practice Satellite Workshop of MODELS, A., no. 166, pp. 1-16, [Online], Available: https://pdfs.semanticscholar.org/f608/40351e4f18c6513465956361b99a0eabb148.pdf, 2005.

[30] J. Greenyer and J. Rieke, "Applying Advanced TGG Concepts for a Complex Transformation of Sequence Diagram Specifications to Timed Game Automata," Proc. of the International Symposium on Applications of Graph Transformations with Industrial Relevance, pp. 222-237, Springer, Berlin, Heidelberg, 2011.

[31] F. Budinsky, D. Steinberg, E. Ellersick, T. J. Grose and E. Merks, Eclipse Modeling Framework: A Developer's Guide, Addison-Wesley Professional, 2004.

[32] R. Elmansouri, S. Meghzili, A. Chaoui, A. Belghiat and O. Hedjazi, "Transformation Rules of UML Activity Diagrams to Pi-calculus Using TGG," Internal Report, MFGL Team, MISC Laboratory, University Constantine 2-Abdelhamid Mehri, Algeria, [Online], Available: https://misc-lab.org/en/teams/show/MFGL.

[33] D. Bisztray, K. Ehrig and R. Heckel, "Case Study: UML to CSP Transformation," Applications of Graph Transformation with Industrial Relevance, [Online], Available: https://www.informatik.uni-marburg.de/~swt/agtive-contest/UML-to-CSP.pdf, 2007.

[34] SMLNJ, "Standard ML of New Jersey," [Online], Available: http://smlnj.org.