up: Publications |
Abstract |
Formal methods are increasingly used in software engineering. They offer a formal frame that guarantees the correctness of developments. 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 provably correct development, and manipulate its components in a graphical/textual editor.
This paper constitutes a first step towards using Model Driven Engineering
(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.
Online Copy |
Conference version: PDF
Extended version: PDF
BibTeX Entry |
@inproceedings{djeddai12:_case_study_combin_formal_verif, author = {Selma Djeddai and Mohamed Mezghiche and Martin Strecker}, title = {A Case Study in Combining Formal Verification and Model-Driven Engineering}, booktitle = {Proceedings of the 8th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Kherson, Ukraine, June 6-10, 2012}, year = {2012}, pages = {275-289}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, ee = {http://ceur-ws.org/Vol-848}, url = {https://www.irit.fr/~Martin.Strecker/Publications/smsv2012.html}, }
Last modified: Thu Dec 6 14:16:01 CET 2012 |