Extending specification patterns for verification of parametric traces - Université Grenoble Alpes Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Extending specification patterns for verification of parametric traces

Résumé

This article proposes a temporal and parametric specification language (ParTraP) developed for the verification of execution traces. The language extends specification patterns with nested scopes, real-time and first-order quantification over the data inside a JSON trace, while remaining pragmatic. Its design was directed by a case study in the medical field (computer aided surgery). The paper briefly presents the case study and details the design rationale, syntax and semantics of the language. The language has been implemented and several properties have been successfully evaluated over a corpus of 100 surgery traces.
Fichier principal
Vignette du fichier
formalise.pdf (1.01 Mo) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02004378 , version 1 (25-10-2019)

Identifiants

Citer

Yoann Blein, Yves Ledru, Lydie Du-Bousquet, Roland Groz. Extending specification patterns for verification of parametric traces. the 6th Conference on Formal Methods in Software Engineering (FormaliSE'18), Jun 2018, Gothenburg, Sweden. pp.10-19, ⟨10.1145/3193992.3193998⟩. ⟨hal-02004378⟩
66 Consultations
203 Téléchargements

Altmetric

Partager

Gmail Mastodon Facebook X LinkedIn More