Abstract
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]