Validation of Formal Specifications through Transformation and Animation

Atif Mashkoor 1 Jean-Pierre Jacquot 2
2 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : —A significant impediment to the uptake of formal refinement-based methods among practitioners is the challenge of validating that the formal specifications of these methods capture the desired intents. Animation of specifications is widely recognized as an effective way of addressing such validation. However, animation tools are unable to directly execute (and thus animate) the typical uses of several of the specification constructs often found in ideal formal specifications. To address this problem we have developed transformation heuristics that, starting with an ideal formal specification, guide its conversion into an animatable form. We show several of these heuristics, and address the need to prove that the application of these transformations preserves the relevant behavior of the original specification. Portions of several case studies illustrate this approach
Type de document :
Article dans une revue
Requirements Engineering, Springer Verlag, 2017, 22 (4), pp.433-451. 〈10.1007/s00766-016-0246-6〉
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01262115
Contributeur : Jean-Pierre Jacquot <>
Soumis le : mardi 26 janvier 2016 - 11:41:52
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08
Document(s) archivé(s) le : mercredi 27 avril 2016 - 13:21:13

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot. Validation of Formal Specifications through Transformation and Animation. Requirements Engineering, Springer Verlag, 2017, 22 (4), pp.433-451. 〈10.1007/s00766-016-0246-6〉. 〈hal-01262115〉

Partager

Métriques

Consultations de la notice

220

Téléchargements de fichiers

98