Extending specification patterns for verification of parametric traces

Yoann Blein 1 Yves Ledru 1 Lydie Du-Bousquet 1 Roland Groz 1
1 LIG Laboratoire d'Informatique de Grenoble - VASCO
LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

http://hal.univ-grenoble-alpes.fr/hal-02004378
Contributeur : Yves Ledru <>
Soumis le : vendredi 25 octobre 2019 - 15:52:10
Dernière modification le : lundi 28 octobre 2019 - 09:57:05

Fichier

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

Identifiants

Collections

Citation

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⟩

Partager

Métriques

Consultations de la notice

83

Téléchargements de fichiers

87