A Case Study in Combining Formal Verification and Model-Driven Engineering
Selma Djeddai, Mohamed Mezghiche, Martin Strecker · 2012
Formal methods are increasingly used in software engineer- ing. They offer a formal frame that guarentees the correctness of devel- opments. However, they use complex notations that might be difficult to understand for unaccustomed users. It thus becomes interesting to formally specify the core components of a language, implement a prov- ably correct development, and manipulate its components in a graphi- cal/textual editor. This paper constitutes a first step towards using Model Driven Engineer- ing (MDE) technology in an interactive proof development. It presents a transformation process from functional data structures, commonly used in proof assistants, to Ecore Models. The transformation is based on an MDE methodology. The resulting meta-models are used to generate graphical or textual editors. We will take an example to illustrate our approach: a simple domain specific language. This guiding example is a Java-like language enriched with assertions.