653 articles – 968 Notices  [english version]

hal-00544261, version 1

Transformational Heuristics for Animation - Towards Stepwise Validation of Specications

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

(07/12/2010)

Résumé : 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.

  • 1 :  DEDALE (LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Informatique/Génie logiciel
 
  • hal-00544261, version 1
  • oai:hal.archives-ouvertes.fr:hal-00544261
  • Contributeur : 
  • Soumis le : Mardi 7 Décembre 2010, 15:40:03
  • Dernière modification le : Mercredi 1 Juin 2011, 16:39:46