Accéder directement au contenu Accéder directement à la navigation
Thèse

ParTraP: A Language for the Specification and Runtime Verification of Parametric Properties

Yoann Blein 1
1 VASCO [2016-2019] - Validation de Systèmes, Composants et Objets logiciels [2016-2019]
LIG [2016-2019] - Laboratoire d'Informatique de Grenoble [2016-2019]
Résumé : La vérification à l'exécution est une technique prometteuse pour améliorer la sûreté des systèmes complexes. Ces systèmes peuvent être instrumentés afin qu'ils produisent des traces d'exécution permettant d'observer leur utilisation dans des conditions réelles. Un défi important est de fournir aux ingénieurs logiciel un langage formel simple adapté à l'expression des exigences les plus importantes. Dans cette thèse, nous nous intéressons à la vérification de dispositifs médicaux. Nous avons effectué l'analyse approfondie d'un dispositif médical utilisé mondialement afin d'identifier les exigences les plus importantes, ainsi que la nature précise des traces d'exécution qu'il produit. À partir de cette analyse, nous proposons ParTraP, un langage défini formellement et dédié à la spécification de propriétés sur des traces finies. Il a été conçu pour être accessible à des ingénieurs logiciels non qualifiés en méthodes formelles grâce à sa simplicité et son style déclaratif. Le langage étend les patrons de spécification initialement proposé par Dwyer et. al. avec des opérateurs paramétriques et temps-réel, des portées emboîtable, et des quantificateurs de premier ordre. Nous proposons également une technique de mesure de couverture pour ParTraP, et que le niveau de couverture d'une propriété temporelle permet de mieux la comprendre, ainsi que le jeu de traces sur lequel elle est évaluée. Finalement, nous décrivons l'implémentation d'un environnement de développement intégré pour ParTraP, qui est disponible sous une licence libre.
Liste complète des métadonnées

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

https://hal.univ-grenoble-alpes.fr/tel-02269062
Contributeur : Sandrine Corvey-Biron <>
Soumis le : jeudi 22 août 2019 - 11:01:57
Dernière modification le : mercredi 5 août 2020 - 03:01:56
Document(s) archivé(s) le : vendredi 10 janvier 2020 - 18:38:02

Fichier

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

Identifiants

  • HAL Id : tel-02269062, version 1

Collections

Citation

Yoann Blein. ParTraP: A Language for the Specification and Runtime Verification of Parametric Properties. Software Engineering [cs.SE]. Université Grenoble Alpes, 2019. English. ⟨tel-02269062⟩

Partager

Métriques

Consultations de la notice

151

Téléchargements de fichiers

165