Model Checking and Code Generation for UML Diagrams Using Graph Transformation

UML is considered as the standard for object-oriented modelling language adopted by the ObjectManagement Group. However, UML has been criticized due to the lack of formal semantics and theambiguity of its models. In other hands, UML models can be mathematically verified and checked by usingits equivalent formal representation. So, in this paper, we propose an approach and a tool based on graphtransformation to perform an automatic mapping for verification purposes. This transformation aims tobridge the gap between informal and formal notations and allows a formal verification of concurrent UMLmodels using Maude language. We consider both static (Class Diagram) and dynamic (StateChart andCommunication Diagrams) features of concurrent object-oriented system. Then, we use Maude LTL ModelChecker to verify the formal model obtained (Automatic Code Generation Maude). The meta-modellingAToM3 tool is used. A case study is presented to illustrate our approach.