Scaling Up with Event-B: A Case Study

Faqing Yang 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Ability to scale up from toy examples to real life problems is a crucial issue for formal methods. Formalizing a algorithm used in vehicle automation (platooning control) in a certification perspective, we had the opportunity to study the scaling up when going from a (toy) model in 1D to a (more realistic) model in 2D. The formalism, Event-B, belongs to the family of mathematical state based methods. Increase was quantitative: 3 times more events and 4 times more proofs; and qualitative: trigonometric functions and integrals are used. Edition and verification of the specification scale up well. The crucial part of the work was the adaptation of the mathematical and physical model through standard heuristics. The validation of temporal properties and behaviors do not scale up so well. Analysis of the difficulties suggests improvements in both tool support and formalism.
Type de document :
Communication dans un congrès
Mihaela Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi. Third NASA Formal Methods Symposium, Apr 2011, Pasadena, United States. 2011, 〈10.1007/978-3-642-20398-5_31〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00604687
Contributeur : Faqing Yang <>
Soumis le : mercredi 29 juin 2011 - 15:17:42
Dernière modification le : mardi 24 avril 2018 - 13:36:50
Document(s) archivé(s) le : vendredi 30 septembre 2011 - 02:23:31

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Faqing Yang, Jean-Pierre Jacquot. Scaling Up with Event-B: A Case Study. Mihaela Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi. Third NASA Formal Methods Symposium, Apr 2011, Pasadena, United States. 2011, 〈10.1007/978-3-642-20398-5_31〉. 〈inria-00604687〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

231

Téléchargements de fichiers

404

Contact


archive-ouverte@inria.fr