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.
الكلمات المفتاحية :
Model-driven engineering
Graph transformation
Transformation correctness
Model checker
GROOVE
Software systems
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 -