Abstract
This paper presents our position and experience on integrating \emphformal methods with the \emphModel-driven Engineering
(MDE) approach to software development. Both these two approaches have advantages and disadvantages, and we here show how
the advantages of one can be exploited to cover or weaken the disadvantages of the other. We also propose an \emphin-the-loop
integration which allows the development of a general framework for software engineering where rigorousness and preciseness
of formal methods are combined with flexibility and automation of the MDE. We discuss the feasibility of unifying these two
separate worlds, referring to our experience on integrating the Abstract State Machine formal method with the Eclipse Modeling
Framework supporting MDE facilities.
[download the pdf file] [DOI]