Transformational Heuristics for Animation - Towards Stepwise Validation of Specications

Atif Mashkoor (1) , Jean-Pierre Jacquot (1)

1 DEDALE - Development of specifications

In formal methods, a key idea to assess that an implementation is correct is to break its verification into smaller proofs associated with each refinement step. Likewise, the technique of animation could be used during refinement process to break its validation into smaller assessments. Animating an abstract specification often requires to alter it in order to make it animatable. So we design a set of heuristics whose application transforms non-animatable specifications into animatable specifications and then based on these transformational heuristics, we develop a rigorous validation framework for stepwise validation of formal specifications.

Domaines: Génie logiciel [cs.SE]

Atif Mashkoor, Jean-Pierre Jacquot. Transformational Heuristics for Animation - Towards Stepwise Validation of Specications. 2010. ⟨hal-00544261⟩