Experiences in Model Driven Verification of Behavior with UML

International audienceModel Driven Development (MDD) focuses on the intensive use of models during software development. In this paradigm, models are the central development artifact: transformations are used to derive executable programs, or tests for a given platform. This makes building quality models a cost-effective approach, as the models can be reused for many analysis or generation goals, and not just document a design. However, high quality models are needed for the approach to be successful. Hence the goal of performing analysis of high-level behavioral specifications such as UML, to enhance their quality and detect defects or ensure desired behavior.High-level specifications provide many facilities to handle large specifications (such as hierarchical structuring mechanisms) and provide sophisticated features to handle programming language’s rich semantics. However, the price of these features is that these specifications are difficult to analyse, the semantics are not necessarily formally defined, and the complexity of the language features usually limits analysis to manual inspection, or in the best cases simulation.On the other hand, formal specifications have been developed specifically with analysis purposes in mind. In particular, model checking is an automatic approach suitable to analyse formally defined behaviors. However, formal specifications languages such as CSP, PROMELA, Petri nets, etc. have a steep learning curve, and are not cost effective since they are not directly linked to code.In this paper, we explore an approach to integrate formal methods with high-level notations, by translating high-level specifications to formal ones to enable analysis. We are thus bringing Model Driven Engineering to Verification Driven Engineering. We show how this approach was put in practice with UML within the context of the ModelPlex project