Transformation Heuristics for Formal Requirements Validation by Animation

Atif Mashkoor 1 Jean-Pierre Jacquot 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Safety critical software systems are regulated by stringent certification requirements. The use of formal methods is the part of standard recommendations in particular for higher safety integrity levels. An important issue with formal methods is the problem of the validation of requirements: do they accurately capture the stakeholder needs? While proof tools guarantee the consistency of a specification, they are of little help to check if the specification models the desired behavior. This paper addresses the problem of the validation of Event-B specifications by animation. Once the specifications have been verified using the RODIN platform, they have to be transformed in order to be animated by the Brama animator. We propose transformation heuristics in order to produce a derived animatable specification which may be non-provable, but exhibiting the same behavior as the original specification.
Type de document :
Communication dans un congrès
2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems - SafeCert 2009, Mar 2009, York, United Kingdom. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00374082
Contributeur : Atif Mashkoor <>
Soumis le : mardi 7 avril 2009 - 19:06:17
Dernière modification le : mardi 24 avril 2018 - 13:29:55
Document(s) archivé(s) le : vendredi 12 octobre 2012 - 16:25:16

Fichier

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

Identifiants

  • HAL Id : inria-00374082, version 1

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot, Jeanine Souquières. Transformation Heuristics for Formal Requirements Validation by Animation. 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems - SafeCert 2009, Mar 2009, York, United Kingdom. 2009. 〈inria-00374082〉

Partager

Métriques

Consultations de la notice

340

Téléchargements de fichiers

166