Validation of Formal Specifications through Transformation and Animation - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles Requirements Engineering Year : 2017

Validation of Formal Specifications through Transformation and Animation

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
Fichier principal
Vignette du fichier
main.pdf (1.94 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01262115 , version 1 (26-01-2016)

Identifiers

Cite

Atif Mashkoor, Jean-Pierre Jacquot. Validation of Formal Specifications through Transformation and Animation. Requirements Engineering, 2017, 22 (4), pp.433-451. ⟨10.1007/s00766-016-0246-6⟩. ⟨hal-01262115⟩
148 View
425 Download

Altmetric

Share

Gmail Facebook X LinkedIn More