jiaria10 Gargantini, Angelo Riccobene, Elvinia Scandurra, Patrizia

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

in International Journal On Advances in Software, vol. 1&2 (2010): 1--18

The use of \emphformal methods (FMs), based on rigorous mathematical foundations, is essential for system specification and proof, especially for safety critical systems. On the other hand, \emphModel-driven Engineering (MDE) is emerging as new approach to software development based on the systematic use of models as primary artefacts throughout the engineering life-cycle by combining domain-specific modeling languages (DSMLs) with model transformers, analyzers, and generators. In this paper, we present our position and experience on combining flexibility and automation of the MDE approach with rigorousness and preciseness of FMs to achieve significant boosts in both productivity and quality in model-driven design and analysis of software and systems. We propose an \emphin-the-loop integration where, on one hand, MDE principles are used to engineer a language and a tool-set around a formal method for its practical adoption in systems development life cycle, and, on the other hand, the same FM 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 EMF framework and formal system analysis by ASMs in a seamless and systematic way, as shown by a concrete case study.

[download the pdf file]

My sw links