Browsing by Author "Chaoui, Allaoua"

Now showing 1 - 3 of 3

Access status: Open Access ,
A UML 2.0 activity diagrams/csp integrated approach for modeling and verification of software systems
(Wydawnictwa AGH, 2021) Elmansouri, Raida; Meghzili, Said; Chaoui, Allaoua
This paper proposes an approach that integrates UML 2.0 Activity Diagrams (UML2-ADs) and the communicating sequential process (CSP) for modeling and verifying software systems. A UML2-AD is used for modeling a software system, while a CSP is used for verification purposes. The proposed approach consists of another way of transforming UML2-AD models to CSP models. It also focuses 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-modeling is realized using the AToMPM tool, while the model transformation and the correctness of its properties are realized using the GROOVE tool. Finally, we illustrated this approach through a case study.
Access status: Open Access ,
Automatic bridge between BPMN models and UML activity diagrams based on graph transformation
(Wydawnictwa AGH, 2022) Rahmoune, Yasmina; Chaoui, Allaoua
Model-driven engineering (MDE) provides the available tools, concepts, and languages for creating and transforming models. One of the most important successes of MDE is model transformation, it permits the transformion of models that are used by one community to equivalent models that can be used by another one. Moreover, each community of developers has its own tools for verification, testing, and test-case generation. Hence, a developer of one community who moves to another community needs a transformation process from the second community to his/her own community and vice versa. Therefore, the target community can benefit from the expertise of the source one, and the developers do not begin from zero. In this context, we propose an automatic transformation in this paper for creating a bridge between the BPMN and UML communities. We propose an approach and a visual tool for the automatic transformation of BPMN models to UML activity diagrams (UML-AD). The proposed approach is based on meta-modeling and graph transformation and uses the AToM3 tool. Indeed, we were inspired by the OMG meta-models of BPMN and UML-AD and implemented versions of both meta-models using AToM3 . This latter one allows for the automatic generation of a visual-modeling tool for each proposed meta-model. Based on these two meta-models, we propose a graph grammar that is composed of 58 rules that perform the transformation process. The proposed approach is illustrated through three case studies.
Access status: Open Access ,
Formalization and analysis of UML 2.0 interaction overview diagram using maude rewriting logic language
(Wydawnictwa AGH, 2024) Djaoui, Chafika; Chaoui, Allaoua
The visual modeling language UML embodies object-oriented design principles. It provides a standard way to visualize the design of a system. It exploits a rich set of well-defined graphical notations for creating abstract models. However, the power of UML is lessened through partially specified formal semantics. Indeed, UML notations are semi-formal and do not lead to fully formalized and executable semantics. Fortunately, UML diagrams are prone to early formalization. Formal methods are a valuable tool that can help overcome the UML constructs’ shortage of firm semantics. It is a powerful way to ascribe precise semantics to the graphical notations used in UML diagrams and models. Our work aims to support the semantics of the UML Interaction Overview Diagram. It introduces an approach to leveraging the strengths of the Maude Rewriting Logic language as a formal specification language. The proposal relies on a model-driven engineering approach. It aims to automate the UML Interaction Overview Diagram’s mapping to a Maude language specification. The Maude language and its linked tools, including the Maude Model Checker, are used to analyze and verify the resulting Maude specification. Finally, an application example shows the feasibility and benefits of the proposed approach.