|
Depot Institutionnel de l'UMBB >
Publications Scientifiques >
Communications Internationales >
Veuillez utiliser cette adresse pour citer ce document :
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/1679
|
| Titre: | A case study in combining formal verification and model-driven engineering |
| Auteur(s): | Djeddai, S.
Mezghiche, Mohamed
Strecker, M. |
| Mots-clés: | Formal Methods
Model Driven Engineering
Model Transformation
Formal methods
Industrial applications
Industrial research
Knowledge management
Software engineering
Verification
Domain specific languages
Formal verifications
Interactive proof development
Model transformation
Model-driven Engineering
Proof assistant
Transformation process
Java programming language |
| Date de publication: | 2012 |
| Editeur: | CEUR-WS |
| Référence bibliographique: | 8th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, ICTERI 2012; Kherson; Ukraine; 6 June 2012 through 10 June 2012; Code 102006 |
| Collection/Numéro: | CEUR Workshop Proceedings /Vol. 848, 2012;pp. 275-289 |
| Résumé: | 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. |
| URI/URL: | http://dlibrary.univ-boumerdes.dz:8080123456789/1679 |
| ISSN: | 16130073 |
| Collection(s) : | Communications Internationales
|
Fichier(s) constituant ce document :
|
Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.
|
