A UML 2.0 activity diagrams/csp integrated approach for modeling and verification of software systems

• Autorzy: Elmansouri Raida , Meghzili Said , Chaoui Allaoua

Identyfikatory

DOI

10.7494/csci.2021.22.2.3478

• Języki publikacji: EN

Abstrakty

EN

This paper proposes an approach that integrates UML 2.0 Activity Diagrams (UML2-ADs) and the communicating sequential process (CSP) for modeling and verifying software systems. A UML2-AD is used for modeling a software system, while a CSP is used for verification purposes. The proposed approach consists of another way of transforming UML2-AD models to CSP models. It also focuses on checking the correctness of some properties of the transformation itself. These properties are specified using linear temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on model -driven engineering (MDE). The meta-modeling is realized using the AToMPM tool, while the model transformation and the correctness of its properties are realized using the GROOVE tool. Finally, we illustrated this approach through a case study.

Słowa kluczowe

EN

model-driven engineering; graph transformation; transformation correctness; model checker; groove; software systems

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2021
• Tom: T. 22 (2)
• Strony: 209–233
• Opis fizyczny: Bibliogr. 27 poz., rys.

Twórcy

autor

Elmansouri Raida

• MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria

autor

Meghzili Said

• MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria

autor

Chaoui Allaoua

• MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria

Bibliografia

• [1] Amrani M., Combemale B., L´ucio L., Selim G., Dingel J., Le Traon Y., Vangheluwe H., Cordy J.R.: Formal Verification Techniques for Model Transformations: A Tridimensional Classification, The Journal of Object Technology, vol. 14(3), pp. 1–43, 2015. doi: 10.5381/jot.2015.14.3.a1.
• [2] AToMPM project: 2019. http://www-ens.iro.umontreal.ca/∼syriani/atompm/ atompm.htm.
• [3] Bisztray D., Ehrig K., Heckel R.: Case study: UML to CSP Transformation, 2007. AGTIVE 2007 Tool Contest Overview. https://www.informatik.uni-marburg.de/ ∼swt/agtive-contest/UML-to-CSP.pdf.
• [4] Brenas J.H., Echahed R., Strecker M.: Ensuring Correctness of Model Transformations While Remaining Decidable. In: International Colloquium on Theoretical Aspects of Computing, pp. 315–332, Springer, 2016.
• [5] Busser de J.: Model checking AToMPM transformation systems with GROOVE, Technical report, University of Antwerp, 2015.
• [6] Calegari D., Szasz N.: Verification of Model Transformations: A Survey of the State-of-the-Art, Electronic Notes in Theoretical Computer Science, vol. 292, pp. 5–25, 2013.
• [7] Cuadrado J.S., Guerra E., de Lara J., Claris´o R., Cabot J.: Translating Target to Source Constraints in Model-to-Model Transformations. In: 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 12–22, IEEE, 2017. doi: 10.1109/MODELS.2017.12.
• [8] Ehrig H., Hermann F., Sartorius C.: Completeness and Correctness of Model Transformations Based on Triple Graph Grammars With Negative Application Conditions, Electronic Communications of the EASST, vol. 18, 2009.
• [9] Ghamarian A.H., Mol de M., Rensink A., Zambon E., Zimakova M.: Modelling and analysis using GROOVE, International Journal on Software Tools for Technology Transfer, vol. 14(1), pp. 15–40, 2012. doi: 10.1007/s10009-011-0186-x.
• [10] Gogolla M., Hamann L., Hilken F.: Checking Transformation Model Properties with a UML and OCL Model Validator. In: Proceedings of 3rd International Workshop on Verification of Model Transformation (VOLT’2014), pp. 16–25, 2014.
• [11] GROOVE Home Page: 2019. http://GROOVE.cs.utwente.nl/.
• [12] Guerra E., Lara de J., Wimmer M., Kappel G., Kusel A., Retschitzegger W., Schonbock J., Schwinger W.: Automated verification of model transformations based on visual contracts, Automated Software Engineering, vol. 20, pp. 5–46, 2013. doi: 10.1007/s10515-012-0102-y.
• [13] Hoare C.A.R.: Communicating sequential processes, Communications of the ACM, vol. 21(8), pp. 666–677, 1978. doi: 10.1145/359576.359585.
• [14] Lengyel L., Charaf H.: Test-driven verification/validation of model transformations, Frontiers of Information Technology & Electronic Engineering, vol. 16(2), pp. 85–97, 2015.
• [15] Lucio L., Amrani M., Dingel J., Lambers L., Salay R., Selim G.M., Syriani E., Wimmer M.: Model transformation intents and their properties, Software & Systems Modeling, vol. 15(3), pp. 647–684, 2016.
• [16] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: Transformation and validation of BPMN models to Petri nets models using GROOVE. In: 2016 International Conference on Advanced Aspects of Software Engineering (ICAASE), pp. 22–29, IEEE, 2016.
• [17] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL. In: 2017 IEEE International Conference on Information Reuse and Integration (IRI), pp. 419–426, IEEE, 2017.
• [18] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: Verification of Model Transformations Using Isabelle/HOL and Scala, Information Systems Frontiers, vol. 21(1), pp. 45–65, 2019.
• [19] Penker M.: Business Modeling With UML: Business Patterns at Work, John Wiley & Sons, 2000.
• [20] Putter de S., Wijs A.: A formal verification technique for behavioural model-to-model transformations, Formal Aspects of Computing, vol. 30(1), pp. 3–43, 2018. doi: 10.1007/s00165-017-0437-z.
• [21] Rahim L.A., Whittle J.: A survey of approaches for verifying model transformations, Software & Systems Modeling, vol. 14(2), pp. 1003–1028, 2015.
• [22] Rensink A.: The GROOVE Simulator: A Tool for State Space Generation. In: International Workshop on Applications of Graph Transformations with Industrial Relevance, pp. 479–485, Springer, 2003. doi: 10.1007/978-3-540-25959-6 40.
• [23] Rozenberg G.: Handbook of Graph Grammars and Computing by Graph Transformation. Volume 1: Foundations, World Scientific, 1997. doi: 10.1142/3303.
• [24] Schurr A.: Specification of Graph Translators With Triple Graph Grammars. In: International Workshop on Graph-Theoretic Concepts in Computer Science, pp. 151–163, Springer, 1994.
• [25] Silva da A.R.: Model-driven engineering: A survey supported by the unified conceptual model, Computer Languages, Systems & Structures, vol. 43, pp. 139–155, 2015. doi: 10.1016/j.cl.2015.06.001.
• [26] UML diagrams: Process Shopping Order. UML Activity Diagram Example: 2015. https://www.uml-diagrams.org/shopping-process-order-uml-activitydiagram-example.html?context=activity-examples.
• [27] Unified Modeling Language Specification, version 2.0: 2005. https://www.omg. org/spec/UML/2.0/About-UML/.

Uwagi

PL

„Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).”