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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download
Contributor : Atif Mashkoor <>
Submitted on : Tuesday, December 6, 2011 - 4:06:29 PM
Last modification on : Tuesday, April 24, 2018 - 1:34:58 PM
Long-term archiving on : Monday, December 5, 2016 - 12:25:01 AM


Files produced by the author(s)


  • HAL Id : inria-00392939, version 2



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. ⟨inria-00392939v2⟩



Record views


Files downloads