H. Hamrouche, A. Chaoui and S. Mazouzi. 2022. A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams. COMPUTING AND INFORMATICS, 41 (December 2022), Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia, 1284-1309. DOI: https://doi.org/10.31577/cai_2022_5_1284.

Hamrouche, H., Chaoui, A. & Mazouzi, S. (2022, December). A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams. COMPUTING AND INFORMATICS, 41, Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia, 1284-1309. DOI: https://doi.org/10.31577/cai_2022_5_1284

H. Hamrouche, A. Chaoui and S. Mazouzi, "A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams". COMPUTING AND INFORMATICS, vol. 41, Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia, pp. 1284-1309, December, 2022. DOI: https://doi.org/10.31577/cai_2022_5_1284.

@article{misc-lab-415,
author = {Hamrouche, Houda and Chaoui, Allaoua and Mazouzi, Smaine},
title = {A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams},
journal = {COMPUTING AND INFORMATICS},
volume = {41},
issn = {1335-9150},
pages = {1284--1309},
publisher = {Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia},
year = {2022},
month = {December},
doi = {10.31577/cai\_2022\_5\_1284},
url = {https://www.cai.sk/ojs/index.php/cai/article/view/2022\_5\_1284},
keywords = {Unified Modeling Language 2.0, Hoare’s communicating sequential processes, graph grammar, meta-modeling, model checker, AToM3 tool}
}

TI  - A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams
AU  - H. Hamrouche
AU  - A. Chaoui
AU  - S. Mazouzi
PY  - 2022
SN  - 1335-9150
JO  - COMPUTING AND INFORMATICS
VL  - 41
SP  - 1284
EP  - 1309
PB  - Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia
AB  - Unified Modeling Language (UML) 2.0 Sequence Diagrams (UML 2.0 SD) are used to describe interactions in software systems. These diagrams must be verified in the early stages of software development process to guarantee the production of a reliable system. However, UML 2.0 SD lack formal semantics as all UML specifications, which makes their verification difficult, especially if we are modeling a critical system where the automation of verification is necessary. Communicating Sequential Processes (CSP) is a formal specification language that is suited for analysis and has many automatic verification tools. Thus, UML and CSP have complementary aspects, which are modeling and analysis. Recently, a formalization of UML 2.0 SD using CSP has been proposed in the literature; however, no automation of that formalization exists. In this paper, we propose an approach on the basis of the above formalization and a visual modeling tool to model and automatically transform UML 2.0 SD to CSP ones; thus, the existing CSP model checker can verify them. This approach aims to use UML 2.0 SD for modeling and CSP and its tools for verification. This approach is based on graph transformation, which uses AToM3 tool and proposes a metamodel of UML 2.0 SD and a graph grammar to perform the mapping of the latter into CSP. Failures-Divergence Refinement (FDR) is the model checking tool used to verify the behavioral properties of the source model transformation such as deadlock, livelock and determinism. The proposed approach and tool are illustrated through a case study.
KW  - Unified Modeling Language 2.0
KW  - Hoare’s communicating sequential processes
KW  - graph grammar
KW  - meta-modeling
KW  - model checker
KW  - AToM3 tool
DO  - 10.31577/cai_2022_5_1284
UR  - https://www.cai.sk/ojs/index.php/cai/article/view/2022_5_1284
ID  - misc-lab-415
ER  -