Towards automatic generation of formal specifications for UML consistency verification

With the growth of systems complexity the need for verifying the behavior of systems is increasing. UML per se provides no means to check model consistency. However, UML models can be checked if they are converted into their equivalent formal representation. In this paper, we propose an approach based on Model-to-Text transformation to perform a semi-automatic mapping for verification of concurrent UML models using MERL language and MetaEdit+ tool. State machine is transformed into SMV model description and activity diagram is transformed into LTL formulas. Then, we use NuSMV model checker to verify the obtained formal specification. To evaluate the work, a case study of the ordering system is presented to illustrate our approach. A mapping method to check the consistency of state machines with related activity diagrams at early stages of system development is the main result of our work.

Keywords:

UML diagram , Model transformation , MetaEdit+ , Model checking ,