Open AccessGenerating Maude Specifications from M-UML Statechart Diagrams
Author(s) -
Mourad Kezai,
AUTHOR_ID,
Abdallah Khababa
Publication year - 2022
Publication title -
journal of advanced computational intelligence and intelligent informatics
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.172
H-Index - 20
eISSN - 1343-0130
pISSN - 1883-8014
DOI - 10.20965/jaciii.2022.p0008
Subject(s) - computer science , programming language , uml tool , applications of uml , unified modeling language , class diagram , rewriting , software engineering , software
The unified modeling language (UML) is used for the specification, visualization, and documentation of object-oriented software systems. Mobile UML (M-UML) is an extension of UML that considers mobility aspects, and a mobile statechart is an extension of the standard UML diagram that deals with the requirements for modeling, specifying, and visualizing mobile agent-based systems. However, mobile statecharts inherit UML’s lack of formal notation for analysis and verification purposes. The rewriting logic language Maude is a formal method that deals with mobile computations. In this paper, we propose a formalization of M-UML statechart diagrams using Maude to provide formal semantics for such diagrams. The generated Maude specifications are then used to analyze and check the systems using Maude analytical tools. This approach is illustrated through an example.