Yoann Blein - ParTraP : Un langage pour la spécification et vérification à l'exécution de propriétés paramétriques

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 montrons 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.