Stepwise Validation of Formal Specifications

Atif Mashkoor 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Abstract--This paper explores the possibility to incorporate validation in the stepwise development process of formal specifications. Formal methods based on refinement break the intractable proof of the correctness of implementation into a sequence of many smaller proofs. Likewise, the validation of the specification could be broken into smaller steps associated to refinements with the technique of animation. Animating an abstract specification often requires to alter it in ways that proof obligations cannot be discharged anymore. So, we have developed a process and a set of transformation rules whose application produces an animatable specification which may be non-provable, but which is assured to have the same behavior. Guaranteeing behavioral preservation requires us to define an ad-hoc relationship between specifications based on a kind of trace semantics. 10 rules have been identified and proven to preserve behavior. Observations on the use of the technique on two case-studies are presented.
Type de document :
Communication dans un congrès
The eighteenth Asia-Pacific Software Engineering Conference (APSEC 2011), Dec 2011, Ho Chi Minh City, Vietnam. IEEE, 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00392939
Contributeur : Atif Mashkoor <>
Soumis le : mardi 6 décembre 2011 - 16:06:29
Dernière modification le : mardi 24 avril 2018 - 13:34:58
Document(s) archivé(s) le : lundi 5 décembre 2016 - 00:25:01

Fichier

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

Identifiants

  • HAL Id : inria-00392939, version 2

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot. Stepwise Validation of Formal Specifications. The eighteenth Asia-Pacific Software Engineering Conference (APSEC 2011), Dec 2011, Ho Chi Minh City, Vietnam. IEEE, 2011. 〈inria-00392939v2〉

Partager

Métriques

Consultations de la notice

159

Téléchargements de fichiers

109