Article
المجلة العلمية :
Computing and Informatics (CAI)
ISSN : 1335-9150
الناشر :
Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia
معلومات
الفترة : December 2022
المجلد : 41 العدد : 5
الصفحات : 1284-1309
التفاصيل
A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams
Houda Hamrouche Allaoua Chaoui Smaine Mazouzi
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.
الكلمات المفتاحية :
Unified Modeling Language 2.0 Hoare’s communicating sequential processes Graph grammar Meta-modeling Model checker AToM3 tool
مرجع الإقتباس :
misc-lab-415
DOI :
10.31577/cai_2022_5_1284
الرابط :
Texte intégral
ACM :
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 (CAI), 41, 5 (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.
APA :
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 (CAI), 41(5), Institute of Informatics, SAS Dúbravská cesta 9 845 07 Bratislava Slovakia, 1284-1309. DOI: https://doi.org/10.31577/cai_2022_5_1284
IEEE :
H. Hamrouche, A. Chaoui and S. Mazouzi, "A Graph Transformation Approach for Modeling and Verification of UML 2.0 Sequence Diagrams". Computing and Informatics (CAI), vol. 41, no. 5, 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.
BibTeX :
@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 (CAI)},
volume = {41},
number = {5},
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}
}
RIS :
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 (CAI)
VL - 41
IS - 5
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 -