Article
Journal/Revue :
Computer Science
ISSN : 1508-2806
Publisher :
AGH
Informations
Période : April 2021
Volume : 22 Numéro : 2
Pages : 209–235
Détails
A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems
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.
Mots clés :
Model-driven engineering Graph transformation Transformation correctness Model checker GROOVE Software systems
Réf. de citation :
misc-lab-352
DOI :
10.7494/csci.2021.22.2.3478
Lien :
Texte intégral
ACM :
R. Elmansouri, S. Meghzili and A. Chaoui. 2021. A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems. Computer Science, 22, 2 (April 2021), AGH, 209–235. DOI: https://doi.org/10.7494/csci.2021.22.2.3478.
APA :
Elmansouri, R., Meghzili, S. & Chaoui, A. (2021, April). A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems. Computer Science, 22(2), AGH, 209–235. DOI: https://doi.org/10.7494/csci.2021.22.2.3478
IEEE :
R. Elmansouri, S. Meghzili and A. Chaoui, "A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems". Computer Science, vol. 22, no. 2, AGH, pp. 209–235, April, 2021. DOI: https://doi.org/10.7494/csci.2021.22.2.3478.
BibTeX :
@article{misc-lab-352,
author = {Elmansouri, Raida and Meghzili, Said and Chaoui, Allaoua},
title = {A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems},
journal = {Computer Science},
volume = {22},
number = {2},
issn = {1508-2806},
pages = {209–235},
publisher = {AGH},
year = {2021},
month = {April},
doi = {10.7494/csci.2021.22.2.3478},
url = {https://journals.agh.edu.pl/csci/article/view/3478},
keywords = {model-driven engineering, graph transformation, transformation correctness, model checker, GROOVE, software systems}
}
RIS :
TI  - A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems
AU - R. Elmansouri
AU - S. Meghzili
AU - A. Chaoui
PY - 2021
SN - 1508-2806
JO - Computer Science
VL - 22
IS - 2
SP - 209–235
PB - AGH
AB - 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.
KW - model-driven engineering
KW - graph transformation
KW - transformation correctness
KW - model checker
KW - GROOVE
KW - software systems
DO - 10.7494/csci.2021.22.2.3478
UR - https://journals.agh.edu.pl/csci/article/view/3478
ID - misc-lab-352
ER -