FORMALIZATION AND ANALYSIS OF UML 2.0 INTERACTION OVERVIEW DIAGRAM USING MAUDE REWRITING LOGIC LANGUAGE

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 richset 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 andexecutable semantics. Fortunately, UML diagrams are prone to early formalization. Formal methods are a valuable tool that can help overcome the UMLconstructs’ 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 MaudeRewriting Logic language as a formal specification language. The proposal relies on a model-driven engineering approach. It aims to automate the UMLInteraction 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, anapplication example shows the feasibility and benefits of the proposed approach.