Automatic Formal Model Generation from UML Diagrams – An Implementation Experience

This paper discusses the implementation of a formal method integrated Unified Modeling Language (UML) modelling methodology for the verification of embedded software specifications. The methodology generates mathematically verifiable models, synergising UML visual models with formal methods. The implementation is carried out using Umbrello UML Modeller and Qt. It provides a Graphical User Interface-based tool and a model checking engine, integrated into Umbrello UML Modeller, which can interpret UML diagrams and generate a formal model automatically. The tool architecture has three distinct layers: the UML, Interface, and Formal layers; the Interface layer is the innovative one. GUI is developed for this layer, and all the actions associated with the Interface layer are made available through interactive menus and toolbars.