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 : Formal methods are recommended for the development of software controlled safety critical systems because they support formal verification. However, they raise the issue of validation. Mostly due to poor readability of formal texts, validation is difficult. The key idea of stepwise development process, such as B method is to break the general verification into a sequence of smaller steps, called proof-obligations, associated with each refinement. We aim at “breaking” validation in the similar way. Technology allows us to animate specifications so users can validate them. Verification and validation impose very different constraints on the specification text: the former prefers abstract, non constructive, legible (for specifiers!) texts, the latter requires concrete, constructive, computable texts, for instance. These constraints come from the processes (proofs) or the tools (provers, animators). Validation through animation implies to modify the text: using it on each refinement therefore requires a cost-effective transformation technique.
Document type :
Conference papers
Complete list of metadatas
Contributor : Atif Mashkoor <>
Submitted on : Tuesday, June 9, 2009 - 11:50:42 AM
Last modification on : Thursday, January 11, 2018 - 6:20:08 AM
Long-term archiving on : Monday, October 15, 2012 - 12:10:30 PM


Files produced by the author(s)


  • HAL Id : inria-00392939, version 1


Atif Mashkoor, Jean-Pierre Jacquot. Stepwise Validation of Formal Specifications. The 13th IEEE International High Assurance Systems Engineering Symposium, Nov 2009, Boca Raton, United States. pp.2. ⟨inria-00392939v1⟩



Record views


Files downloads