Proving the Fidelity of Simulations of Event-B Models

Faqing Yang 1 Jean-Pierre Jacquot 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - FM - Department of Formal Methods
Abstract : A major hindrance to the use of formal methods is the difficulty to validate the models, particularly at the early stages of the development. We propose to build simulations: programs automatically generated from the specifications but with user-provided implementations of the non-executable traits of the models. We present such a simulation. Of course, the question of the fidelity of the simulation to the model is raised in such a setting. We provide a formal definition of fidelity and the proof obligations that can be attached to each hand-coded element so that fidelity can be proven.
Type de document :
Communication dans un congrès
The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Jan 2014, Miami, United States. 2014
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00908066
Contributeur : Faqing Yang <>
Soumis le : dimanche 22 décembre 2013 - 07:00:04
Dernière modification le : mardi 24 avril 2018 - 13:30:33
Document(s) archivé(s) le : lundi 24 mars 2014 - 09:15:35

Fichier

hase2014-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00908066, version 1

Collections

Citation

Faqing Yang, Jean-Pierre Jacquot, Jeanine Souquières. Proving the Fidelity of Simulations of Event-B Models. The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Jan 2014, Miami, United States. 2014. 〈hal-00908066〉

Partager

Métriques

Consultations de la notice

359

Téléchargements de fichiers

122