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

https://hal.inria.fr/inria-00392939
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

File

Mashkoor-FMICS09.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00392939, version 1

Citation

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⟩

Share

Metrics

Record views

17

Files downloads

23