JeB: Safe Simulation of Event-B Models in JavaScript

Faqing Yang 1 Jean-Pierre Jacquot 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - FM - Department of Formal Methods
Abstract : The validation of formal models is a challenge for formal methods. We propose JeB, a framework which generates and executes simulations of Event-B models, even highly nondeterministic ones. JeB allows users to safely insert pieces of code to supply deterministic computations where the automatic translation fails. We present how JeB translates Event-B model into JavaScript. We define Fidelity as the formal notion which captures the idea of the correctness of a simulation. We define it through proof-obligations.
Type de document :
Communication dans un congrès
The 20th Asia-Pacific Software Engineering Conference (APSEC), Dec 2013, Bangkok, Thailand. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00908056
Contributeur : Faqing Yang <>
Soumis le : samedi 7 décembre 2013 - 07:00:03
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
Document(s) archivé(s) le : samedi 8 avril 2017 - 02:17:12

Fichier

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

Identifiants

  • HAL Id : hal-00908056, version 1

Collections

Citation

Faqing Yang, Jean-Pierre Jacquot, Jeanine Souquières. JeB: Safe Simulation of Event-B Models in JavaScript. The 20th Asia-Pacific Software Engineering Conference (APSEC), Dec 2013, Bangkok, Thailand. 2013. 〈hal-00908056〉

Partager

Métriques

Consultations de la notice

486

Téléchargements de fichiers

159