Formalization and analysis of UML2.0 interaction overview diagram using maude rewriting logic language

• Autorzy: Djaoui Chafika , Chaoui Allaoua

Identyfikatory

DOI

10.7494/csci.2024.25.3.5964

• Języki publikacji: EN

Abstrakty

EN

The visual modeling language UML embodies object-oriented design principles. It provides a standard way to visualize the design of a system. It exploits a rich set of well-defined graphical notations for creating abstract models. However, the power of UML is lessened through partially specified formal semantics. Indeed, UML notations are semi-formal and do not lead to fully formalized and executable semantics. Fortunately, UML diagrams are prone to early formalization. Formal methods are a valuable tool that can help overcome the UML constructs’ shortage of firm semantics. It is a powerful way to ascribe precise semantics to the graphical notations used in UML diagrams and models. Our work aims to support the semantics of the UML Interaction Overview Diagram. It introduces an approach to leveraging the strengths of the Maude Rewriting Logic language as a formal specification language. The proposal relies on a model-driven engineering approach. It aims to automate the UML Interaction Overview Diagram’s mapping to a Maude language specification. The Maude language and its linked tools, including the Maude Model Checker, are used to analyze and verify the resulting Maude specification. Finally, an application example shows the feasibility and benefits of the proposed approach.

Słowa kluczowe

EN

UML Interaction Overview Diagrams; formal methods; rewriting logic; Maude language; Model-Driven Engineering; MDE; EMF; Sirus; Acceleo

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2024
• Tom: T. 25 (3)
• Strony: 397--419
• Opis fizyczny: Bibliogr. 36 poz., rys., tab., wykr.

Twórcy

autor

Djaoui Chafika

• Mohamed Seddik Ben Yahia University, Department of Computer Science, Jijel, Algeria
• MISC Laboratory, Department of Computer Science and Its Applications, Constantine, Algeria

autor

Chaoui Allaoua

• University Constantine 2-Abdelhamid Mehri, MISC Laboratory, Department of Computer Science and Its Applications, Faculty of Ntic, Constantine, Algeria

Bibliografia

• [1] Andrade E., Maciel P., Callou G., Nogueira B.: Mapping UML Interaction Overview Diagram to Time Petri Net for Analysis and Verification of Embedded Real-Time Systems with Energy Constraints. In: 2008 International Conference on Computational Intelligence for Modelling Control & Automation, pp. 615–620, IEEE, 2008. doi: 10.1109/cimca.2008.44.
• [2] Baresi L., Morzenti A., Motta A., Rossi M.: From Interaction Overview Diagrams to Temporal Logic. In: Models in Software Engineering. Workshops and Symposia at MoDELS 2010, Olso, Norway, October 3–8, 2010, Reports and Revised Selected Papers, pp. 90–104, Springer, 2010. doi: 10.1007/978-3-642-21210-9 9.
• [3] Bennama M., Bouabana-Tebibel T.: Validation environment of UML2 IOD based on hierarchical coloured Petri nets, International Journal of Computer Applications in Technology, vol. 47(2–3), pp. 227–240, 2013. doi: 10.1504/ ijcat.2013.054372.
• [4] Bernardi S., Donatelli S., Merseguer J.: From UML Sequence Diagrams and Statecharts to Analysable Petri Net Models. In: WOSP’02: Proceedings of the 3rd International Workshop on Software and Performance, pp. 35–45, 2002. doi: 10.1145/584369.584376.
• [5] Bernardi S., Merseguer J.: Performance evaluation of UML design with Stochastic Well-formed Nets, Journal of Systems and Software, vol. 80(11), pp. 1843–1865, 2007. doi: 10.1016/j.jss.2007.02.029.
• [6] Bouabana-Tebibel T.: Semantics of the interaction overview diagram. In: 2009 IEEE International Conference on Information Reuse & Integration, pp. 278–283, IEEE, 2009. doi: 10.1109/iri.2009.5211565.
• [7] Bowen J.P., He J.: An algebraic approach to hardware compilation, Modern Formal Methods and Applications, pp. 151–176, 2006.
• [8] Bruni R., Meseguer J.: Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol. 360(1-3), pp. 386–414, 2006. doi: 10.1016/ j.tcs.2006.04.012.
• [9] Clavel M., Dur´an F., Eker S., Escobar S., Lincoln P., Martı-Oliet N., Meseguer J., et al.: Maude manual (version 3.1), 2020. SRI International University of Illinois at Urbana-Champaign. http://maude.lcc.uma.es/maude31-manual-html/ maude-manual.html.
• [10] Clavel M., Dur´an F., Hendrix J., Lucas S., Meseguer J., Olveczky P.: The Maude ¨ formal tool environment. In: T. Mossakowski, U. Montanari, M. Haveraaen (eds.), Algebra and Coalgebra in Computer Science: Second International Conference, CALCO 2007, Bergen, Norway, August 20–24, 2007. Proceedings, pp. 173–178, Springer, 2007. doi: 10.1007/978-3-540-73859-6 12.
• [11] Djaoui C., Kerkouche E., Chaoui A., Khalfaoui K.: A graph transformation approach to generate analysable maude specifications from UML interaction overview diagrams. In: 2018 IEEE International Conference on Information Reuse and Integration (IRI), pp. 511–517, IEEE, 2018. doi: 10.1109/ iri.2018.00081.
• [12] Dobing B., Parsons J.: Dimensions of UML Diagram Use: A Survey of Practitioners, Journal of Database Management (JDM), vol. 19(1), pp. 1–18, 2008. doi: 10.4018/jdm.2008010101.
• [13] Dur´an F., Eker S., Escobar S., Mart´ı-Oliet N., Meseguer J., Rubio R., Talcott C.: Programming and symbolic computation in Maude, Journal of Logical and Algebraic Methods in Programming, vol. 110, 100497, 2020. doi: 10.1016/ j.jlamp.2019.100497.
• [14] Eclipse Foundation: Acceleo, homepage, [Online]. https://www.eclipse.org/ acceleo/. Accessed November 2023.
• [15] Eclipse Foundation: EMF, homepage Eclipse Modelling Framework (EMF), [Online]. https://www.eclipse.dev/modeling/emf/. Accessed November 2023.
• [16] Eclipse Foundation: Sirius, homepage, [Online]. https://www.eclipse.org/sirius/. Accessed November 2023.
• [17] Eker S., Meseguer J., Sridharanarayanan A.: The Maude LTL model checker, Electronic Notes in Theoretical Computer Science, vol. 71, pp. 162–187, 2004. doi: 10.1016/s1571-0661(05)82534-4.
• [18] Frick G., Scherrer B., M¨uller-Glaser K.D.: Designing the software architecture of an embedded system with UML 2.0. In: Software Architecture Description & UML Workshop, 2004.
• [19] Hammal Y.: A Formal Semantics of UML StateCharts by Means of Timed Petri Nets. In: F. Wang (ed.), Formal Techniques for Networked and Distributed Systems – FORTE 2005. 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2–5, 2005, Proceedings, pp. 38–52, Springer, 2005. doi: 10.1007/11562436 5.
• [20] Kerkouche E., Khalfaoui K., Chaoui A.: A rewriting logic-based semantics and analysis of UML activity diagrams: a graph transformation approach, International Journal of Computer Aided Engineering and Technology, vol. 12(2), pp. 237–262, 2020. doi: 10.1504/ijcaet.2020.10026291.
• [21] Kloul L., K¨uster-Filipe J.: From Interaction Overview Diagrams to PEPA Nets, Online Proceedings of the 4th Workshop on Process Algebras and Timed Activities (PASTA’05), vol. 104, 2005.
• [22] de Lara J., Vangheluwe H., Alfonseca M.: Meta-modelling and graph grammars for multi-paradigm modelling in AToM3 , Software & Systems Modeling, vol. 3, pp. 194–209, 2004. doi: 10.1007/s10270-003-0047-5.
• [23] Lilius J., Paltor I.P.: vUML: a Tool for Verifying UML Models. In: 14th IEEE International Conference on Automated Software Engineering, pp. 255–258, 1999. doi: 10.1109/ASE.1999.802301.
• [24] Louati A., Jerad C., Barkaoui K.: On CPN-based verification of hierarchical formalization of UML 2 Interaction Overview Diagrams. In: 2013 5th International Conference on Modeling, Simulation and Applied Optimization (ICMSAO), pp. 1–6, IEEE, 2013. doi: 10.1109/icmsao.2013.6552703.
• [25] McUmber W.E., Cheng B.H.: A general framework for formalizing UML with formal languages. In: Proceedings of the 23rd International Conference on Software Engineering. ICSE 2001, pp. 433–442, IEEE, 2001.
• [26] Meseguer J.: Rewriting Logic and Maude: A Wide-Spectrum Semantic Framework for Object-Based Distributed Systems. In: S.F. Smith, C.L. Talcott (eds.), IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA, pp. 89–117, Springer, 2000. doi: 10.1007/978-0-387- 35520-7 5.
• [27] Meseguer J.: Specifying, Analyzing and Programming Communication Systems in Maude. In: G. Hommel (ed.), Communication-Based Systems: Proceeding of the 3rd International Workshop held at the TU Berlin, Germany, 31 March– 1 April 2000, pp. 93–101, Springer, 2000. doi: 10.1007/978-94-015-9608-4 7.
• [28] Meseguer J.: Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming, vol. 81(7–8), pp. 721–781, 2012. doi: 10.1016/j.jlap.2012.06.003.
• [29] Mishra A.: Dynamic Slicing of UML Interaction Overview Diagram. In: 2019 IEEE 9th International Conference on Advanced Computing (IACC), pp. 125–132, IEEE, 2019. doi: 10.1109/iacc48062.2019.8971586.
• [30] Padua D. (ed.): Encyclopedia of Parallel Computing, Springer Science & Business Media, New York, NY, 2011. doi: 10.1007/978-0-387-09766-4.
• [31] Platt R., Thompson N.: The evolution of UML. In: Encyclopedia of Information Science and Technology, Third Edition, pp. 348–353, IGI Global, 2015.
• [32] Rumbaugh J., Jacobson I., Booch G.: The Unified Modeling Language Reference Manual, 2nd Ed., Addison Wesley Longman Ltd., 2004.
• [33] Steinberg D., Budinsky F., Paternostro M., Merks E.: EMF: eclipse modeling framework, Pearson Education, 2008.
• [34] Storrle H., Hausmann J.H.: Towards a formal semantics of UML 2.0 activities. In: Software Engineering 2005, pp. 117–128, Gesellschaft f¨ur Informatik eV, 2005.
• [35] Wazlawick R.S.: Object-oriented analysis and design for information systems: modeling with UML, OCL, and IFML, Elsevier, 2014.
• [36] Whittle J.: Extending interaction overview diagrams with activity diagram constructs, Software & Systems Modeling, vol. 9, pp. 203–224, 2010.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2024).