Abstract
UML is a semi-formal modeling language for object oriented systems. It is widely accepted and its applications become more and more widespread in real word projects. The UML diagrams suffer from lack of formal semantics which hinders their automatic verification. It is actually a problem that always arises. Formal methods can be used to overcome it. \(\pi \)-calculus is a flexible formal theory with several applications. It offers a rich theory and tools for verification purposes. Thus, this paper presents an approach for capturing and verifying the dynamic behavior of systems using UML diagrams and \(\pi \)-calculus. We illustrate our approach by an example in order to explain it. Then we tackle another small example to show the verification capabilities provided by the approach. An implementation of the approach is presented.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Object Management Group (OMG), Unified Modeling Language (2012). http://www.omg.org/spec/UML/
Milner, R.: Communicating and Mobile Systems: The \(\pi \)-calculus. Cambridge University Press (1999)
Heckel, R., Sauer, S.: Strengthening UML collaboration diagrams by state transformations. Fundamental Approaches to Software Engineering, pp. 109–123. Springer, Berlin (2001)
Ambler, S.W.: The Elements of UML\(^{TM}\)2.0 Style. Cambridge University Press (2005)
Belghiat, A., Chaoui, A., Beldjehem, M.: Capturing and verifying dynamic program behaviour using UML communication diagrams and pi-calculus. In: IEEE International Conference on Information Reuse & Integration (IRI), pp. 318–325. IEEE (2015)
Victor, B.: A Verification Tool for the Polyadic \(\pi \)-Calculus. Licentiate thesis, Department of Computer Systems. Uppsala University (1994)
Victor, B., Moller, F.: The Mobility Workbench - A Tool for the \(\pi \)-calculus. In Dill, D. (eds.) Proceedings of the Conference on Computer-Aided Verification (CAV’94). LNCS, vol. 818, pp. 428–440. Springer Verlag, (1994)
Lano , K., Bicarregui, J.: Formalizing the UML in Structured Temporal Theories. In Rumpe, B., Kilov, H. (eds.) Proceedings of Second ECOOP Workshop on Precise Behavioral Semantics. ECOOP’98. Munich, Germany (1998)
Overgaard, G.: A formal approach to collaborations in the Unified Modeling Language. In: Proceedings of the UML’99—Beyond the Standard. LNCS, vol. 1723, pp. 99–115. Springer-Verlag (1999)
Gomaa, H.: Validation of Dynamic Behavior in UML Using Colored PetriNets. In: Proceedings of the UML2000 (2000)
Saldhana, J., Shatz, S.M.: UML diagrams to object petri net models: an approach for modeling and analysis. In: Proceedings of the International Conference on Software Engineering and Knowledge Engineering (SEKE). pp. 103–110. Chicago (2000)
Dong, Z., He, X.: Integrating UML statechart and collaboration diagrams using hierarchical predicate transition nets. In: Proceedings of pUML, pp. 99–112 (2001)
Elmansouri, R., Chaoui, A., Kerkouche, E., Khalfaoui, K.: From UML statechart and collaboration diagrams to colored petri net models: a graph transformation based approach for modeling and analysis of business processes in virtual enterprises. In: Proceedings of the Fourth South-East European Workshop on Formal Methods. IEEE, Washington, DC, USA (2009)
Merah, E., Messaoudi, N., Saidi, H., Chaoui, A.: Design of ATL rules for transforming UML 2 communication diagrams into buchi automata. Int. J. Softw. Eng. Appl. 7(2), 1–15 (2013)
Motameni, H., Ghassempouri, T.: Transforming fuzzy communication diagram to fuzzy petri net. Am. J. Sci. Res. 16, 62–73 (2011)
Haroonabadi, A., Teshnehlab, M.: A novel method for behavior modeling in uncertain information systems. World Acad. Sci. Eng. Technol. 41, 959–966 (2008)
Gagnon, P., Mokhati, F., Badri, M.: Applying model checking to concurrent UML models. J. Object Technol. 7(1), 59–84 (2008)
Chama, W., Elmansouri, R., Chaoui, A.: Model checking and code generation for UML diagrams using graph transformation. Int. J. Softw. Eng. Appl. (IJSEA), 3(6) (2012)
Fakhroutdinov, K.: (2013). http://www.uml-diagrams.org/
Belghiat, A., Chaoui, A., Maouche, M., Beldjehem, M.: Formalization of mobile UML statechart diagrams using the \(\pi \)-calculus: an approach for modeling and analysis. In Dregvaite, G., Damasevicius, R. (eds.) ICIST 2014, CCIS 465, pp. 236–247. Springer (2014)
Yang, D., Zhang, S.S.: Using \(\pi \)-calculus to formalize UML activity diagrams. In: 10th International Conference and Workshop on the Engineering of Computer-based Systems, pp. 47–54. IEEE Computer Society (2004)
Lam, V.S.W.: On \(\pi \)-calculus semantics as a formal basis for UML activity diagrams. Int. J. Softw. Eng. Knowl. Eng. 18(4), 541–567 (2008)
Kollmann, R., Gogolla, M.: Capturing dynamic program behaviour with UML collaboration diagrams. In Sousa, P., Ebert, J. (eds.) Proceedings of the 5th European Conference on Software Maintenance and Reengineering. IEEE, Los Alamitos (2001)
Object Management Group (OMG), Model Driven Architecture (MDA) (2004). http://www.omg.org/mda/
Karsai, G., Agrawal, A.: Graph transformations in OMG’s model-driven architecture. Applications of Graph Transformations with Industrial Relevance. LNCS, vol. 3062, pp. 243–259. Springer, Berlin (2004)
AToM\(^{3}\) (2002). Home page: http://atom3.cs.mcgill.ca
Python. Home page: http://www.python.org
Acknowledgments
The authors would like to thank Mr. Rachid Echahed (CNRS and University of Grenoble, France) for his advices and comments regarding this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Belghiat, A., Chaoui, A., Beldjehem, M. (2016). Capturing and Verifying Dynamic Systems Behavior Using UML and \(\pi \)-Calculus. In: Bouabana-Tebibel, T., Rubin, S. (eds) Theoretical Information Reuse and Integration. Advances in Intelligent Systems and Computing, vol 446. Springer, Cham. https://doi.org/10.1007/978-3-319-31311-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-31311-5_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-31309-2
Online ISBN: 978-3-319-31311-5
eBook Packages: EngineeringEngineering (R0)