Skip to Main content Skip to Navigation
Reports

Incorporating Animation in Stepwise Development of Formal Specification

Atif Mashkoor 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper explores the possibility to incorporate validation of formal specifications into their step-wise development process. The key idea in formal methods to assess that an implementation is correct is to break the verification into smaller proofs associated with each refinement step. Likewise, the technique of animation could be used with each refinement step to break its validation into smaller assessments. 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 produce an animatable specification which may be non-provable, but which is guaranteed to have the same behavior. 10 rules have been identified; they are presented and discussed with a special emphasis on their validity. We relate how step-wise animation is used in two case studies and what we gain from this.
Document type :
Reports
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00392996
Contributor : Atif Mashkoor <>
Submitted on : Tuesday, June 9, 2009 - 11:55:23 AM
Last modification on : Thursday, May 20, 2021 - 10:09:13 AM
Long-term archiving on: : Monday, October 15, 2012 - 12:10:37 PM

File

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

Identifiers

  • HAL Id : inria-00392996, version 1

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot. Incorporating Animation in Stepwise Development of Formal Specification. [Research Report] 2009, pp.10. ⟨inria-00392996⟩

Share

Metrics

Record views

223

Files downloads

149