A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems

Raida Elmansouri; Said Meghzili; Allaoua Chaoui

doi:10.7494/csci.2021.22.2.3478

Authors

Raida Elmansouri MISC Laboratory, University Constantine 2 – Abdelhamid Mehri; Algeria;
Said Meghzili MISC Laboratory, University Constantine 2 – Abdelhamid Mehri; Algeria;
Allaoua Chaoui MISC Laboratory, University Constantine 2 – Abdelhamid Mehri; Algeria;

DOI:

https://doi.org/10.7494/csci.2021.22.2.3478

Abstract

This paper proposes an approach integrating UML 2.0 Activity Diagrams (UML2-AD) and Communicating Sequential Process (CSP) for modeling and verication of software systems. A UML2-AD is used for modeling a software system while CSP is used for verication purposes. The proposed approach consists of another way of transforming UML2-AD models to Communicating Sequential Process (CSP) models. It focuses also 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-modelling is realized using AToMPM tool while the model transformation and the correctness of its properties are realized using GROOVE tool. Finally, we illustrated this approach through a case study.

Downloads

Download data is not yet available.

References

Unied Modeling Language Specication, version 2.0, 2005. URL https://www.omg.org/spec/UML/2.0/About-UML/.

UML diagrams Activity diagrams Activity examples, 2015. URL https://www.uml-diagrams.org/shopping-process-order-uml-activity-diagram-example.html?context=activity-examples.

GROOVE Home Page, 2019. URL http://GROOVE.cs.utwente.nl/.

Web Site of AToMPM, 2019. URL http://www-ens.iro.umontreal.ca/~syriani/atompm/atompm.htm.

A. R.: The GROOVE Simulator: A Tool for State Space Generation. In: AGTIVE, pp. 479{485. 2003. URL http://dx.doi.org/10.1007/978-3-540-25959-6_40.

A. R.d.S.: Model-driven engineering: A survey supported by the unied conceptual model. In: Computer Languages, Systems Structures, vol. 43, pp. 139-155,2015. URL http://dx.doi.org/10.1016/j.cl.2015.06.001.

Amrani M. C.B.L.L.S.G.D.J.L.T.Y.V.H.C.J.: Formal verication techniques for model transformations: a tridimensional classication. In: Journal of Object Technology, vol. 14(3), pp. 1{43, 2015. URL http://dx.doi.org/10.5381/jot.2015.14.3.a1.

Amrani M. C.B.L.L.S.G.D.J.L.T.Y.V.H.C.J.: Model transformation intents and their properties. In: Software and System Modeling, vol. 15(3), pp. 647-684, 2016. URL http://dx.doi.org/10.1007/s10270-014-0429-x.

Bisztray D. E.K., Heckel R.: Case study: UML to CSP transformation. In: AGTIVE Transformation Contest. 2007. URL http://dx.doi.org/10.1007/978-3-540-89020-1_36. 2019/10/24; 22:29 str. 21/27

Brenas J. H. E.R.S.M.: Ensuring Correctness of Model Transformations While Remaining Decidable. In: Theoretical Aspects of Computing ? ICTAC 2016 13th International Colloquium, pp. 24{31. 2016. URL http://dx.doi.org/10.1007978-3-319-46750-4_18.

Calegari D., Szasz N.: Verication of Model Transformations A Survey of the State-of-the-Art. In: Electronic Notes in Theoretical Computer Science, vol. 292, pp. 5-25, 2015. URL http://dx.doi.org/10.1016/j.entcs.2013.02.002.

Cuadrado J. S. G.E.D.L.J.C.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. 2017. URL http://dx.doi.org/10.1109/MODELS.2017.12.

De Busser J.: Model checking AToMPM transformation systems with Groove. Tech. rep., University of Antwerp, 2015. URL http://dx.doi.org/10.1007/s10270-011-0205-0.

De Putter S. W.A.: A formal verication technique for behavioural model-to-model transformations. In: Formal Aspect Computing, vol. 30(1), pp. 3-43, 2018.URL http://dx.doi.org/10.1007/s00165-017-0437-z.

Ehrig H. H.F.S.C.: Completeness and Correctness of Model Transformations based on Triple Graph Grammars with Negative Application Conditions. In:Journal of Electronic Communications of the EASST, vol. 18, pp. 1-18, 2009. URL http://dx.doi.org/10.14279/tuj.eceasst.18.270.

Ghamarian A.H. D.M.M.R.A.Z.E.Z.M.: Modelling and analysis using GROOVE. In: International Journal on Software Tools for Technology Transfer, vol. 14(1), pp. 15-40, 2012. URL http://dx.doi.org/10.1007/s10009-011-0186-x.

Gogolla M. H.L., Hilken F.: Checking Transformation Model Properties with a UML and OCL Model Validator. In: VOLT, pp. 16{25. 2014. URL http://dx.doi.org/10.1007/978-3-319-21215-9_8.

Guerra E. d.L.J.W.M.K.G.K.A.R.W.S.J.S.W.: Automated verication of model transformations based on visual contracts. In: Automated Software Engineering, vol. 20(1), pp. 5{46, 2013. URL http://dx.doi.org/10.1007/s10515-012-0102-y.

H. E. E., M. P.: Business Modeling with UML: Business Patterns at Work, 2000. URL http://dx.doi.org/10.1093/combul/42.5.30.

Hoare C.: Communicating Sequential Processes. Prentice Hall International Series in Computing Science, 1985. URL http://dx.doi.org/10.1145/359576.359585.

Lengyel L., Charaf H.: Test-driven verication/validation of model transformations. In: Frontiers of IT EE, vol. 16(2), pp. 85{97, 2015. URL http://dx.doi.org/10.1631/FITEE.1400111.

Meghzili S. C.A.S.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. 2016. URL 2019/10/24; 22:29 str. 22/27 http://dx.doi.org/10.1109/ICAASE.2016.7843859.

Meghzili S. C.A.S.M., Kerkouche E.: On the Verication of UML State Machine Diagrams to Colored Petri Nets Transformation using Isabelle/HOL. In: 18th IEEE International Conference on Information Reuse and Integration (IRI 2017). IEEE, 2017. URL http://dx.doi.org/10.1109/IRI.2017.63.

Meghzili S. C.A.S.M., Kerkouche E.: Verication of Model Transformations Using Isabelle/HOL and Scala. In: Information Systems Frontiers Journal, vol. 21(1), pp. 45-65, 2019. URL http://dx.doi.org/10.1007/s10796-018-9860-9.

Rahim A., Whittle J.: A survey of approaches for verifying model transformations. In: Software and Systems Modeling, vol. 14(2), pp. 1003{1028, 2015. URL http://dx.doi.org/10.1007/s10270-013-0358-0.

Rozenberg G.: Handbook of graph grammars and computing by graph transformation, vol. 1. World Scientic, 1997. URL http://dx.doi.org/10.1142/3303.

Schurr A.: Specication of Graph Translators with Triple Graph Grammars. In: WG94 20th Int. Workshop on Graph-Theoretic Concepts in Computer Science,pp. 151-163. 1994. URL http://dx.doi.org/10.1007/3-540-59071-4_45.