Combining Formal Methods and MDE Techniques for Model-driven System Design and Analysis

The use of formal methods, based on rigorous mathematical foundations, is essential for system specification and proof, especially for safety critical systems. On the other hand, Model-driven Engineering (MDE) is emerging as new approach to software development based on the systematic use of models as primary artifacts throughout the engineering life-cycle by combining domain-specific modeling languages (DSMLs) with model transformers, analyzers, and generators. This paper presents our position and experience on combining flexibility and automation of the MDE approach with rigorousness and preciseness of formal methods to achieve significant boosts in both productivity and quality in model-driven design and analysis of software and systems. An in-the-loop integration is proposed where, on one hand, MDE principles are used to engineer a language and a toolset around a formal method for its practical adoption in systems development life cycle, and, on the other hand, the same formal method is used in the same MDE context to endow modeling languages with a precise and (possibly) executable semantics and to perform formal analysis of systems models written in those languages. A concrete scenario of in-the-loop integration is presented in terms of the Abstract State Machine formal method and the Eclipse Modeling Framework. This integration allows system design using the Eclipse Modeling Framework and formal system analysis by Abstract State Machines in a seamless and systematic way, as shown by a concrete case study.