Integrating formal methods with model-driven engineering

In this paper, we present our position and experience on integrating formal methods with the Model-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 in-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.