OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A case study in combining formal verification and model-driven engineering

Djeddai, Selma and Mezghiche, Mohamed and Strecker, Martin A case study in combining formal verification and model-driven engineering. (2013) In: International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification (SMSV 2012) in : 8th International Conference on ICT in Education, Research, and Industrial Applications - ICTERI 2012, 6 June 2012 - 10 June 2012 (Kherson, Ukraine).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-SMSV-paper-1-p-275-289.pdf


Formal methods are increasingly used in software engineering. They offer a formal frame that guarentees 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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to CEUR-WS editor. The definitive version is available at http://ceur-ws.org/Vol-848/. This papers appears in Volume 848 : CEUR Workshop Proceedings 2012. ISSN 1613-0073. The original PDF is available at: http://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-SMSV-paper-1-p-275-289.pdf
HAL Id:hal-01264523
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Other partners > Université M'Hamed Bougara Boumerdes - UMBB (ALGERIA)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:30 Nov 2015 10:12

Repository Staff Only: item control page