Verifying Timed LTL Properties Using Simulink Design Verifier

Les logiciels jouent un rôle de plus en plus important dans les systèmes embarqués notamment dans les domaines de la santé, de l'automobile et de l'avionique. Un objectif important du génie logiciel est d'offrir, aux développeurs, un support ainsi que les outils d'aide à la conception de systèmes fiables nonobstant leur complexité. Dans le but d'atteindre cet objectif, des environnements de développement comme Simulink et SCADE proposent un processus de développement, basé sur des modèles, qui intègre, d'une manière réfléchie, différentes approches et outils de vérification (test, simulation, vérification formelle, évaluation, génération de code, etc). Ils permettent ainsi de concevoir, tester, simuler, vérifier, corriger des modèles puis de générer automatiquement du code à partir de ces modèles. Cette thèse s'intéresse aux méthodes formelles et à l'intégration de celles-ci dans l'environnement de développement Simulink. Les méthodes formelles s'appuient sur des outils mathématiques pour spécifier, par des modèles, le comportement et les propriétés d'un système et prouver qu'il satisfait ses requis. Simulink-Design-Verifier (SLDV) est un outil de vérification formelle, intégré à l'environnement de développement Simulink, qui permet de vérifier des propriétés de sûreté (assertions) sur des modèles Simulink. Cette thèse vise à étendre cette classe de propriétés à des propriétés linéaires LTL (Linear Temporal Logic), LTL temporisé et LTL à base d'événements. Les contributions de cette thèse sont présentées sous forme de trois articles. Le premier article présente une étude de cas qui a permis d'expérimenter l'environnement de développement Simulink, d'identifier ses caractéristiques et ses limitations. Il s'agit de modéliser et vérifier un dispositif médical appelé sonde d'intubation. Une sonde d'intubation est une tubulure mise en place sur un sujet inconscient qui permet notamment d'assurer en permanence le passage de l'air vers les poumons. Ce système est composé de deux ballonnets, deux robinets d'accès pour gonflage manuel, deux capteurs de pression, un distributeur de puissance, une pompe et un réservoir d'air. Tous ces composants sont concurrents et contrôlés par contrôleur programmable décrit par un grafcet. Cet article montre comment utiliser l'environnement Simulink pour, d'une part, modéliser ces différents composants ainsi que leurs interactions, et d'autre part, vérifier formellement des propriétés, afin de s'assurer du bon fonctionnement du système. Cependant, la spécification de certaines propriétés temporelles n'est pas évidente car elles doivent être exprimées sous forme d'assertions. Les articles suivants proposent des blocks canevas pour des propriétés temporelles linéaires. Le deuxième article est une version améliorée et étendue du premier article. Il s'est intéressé à réduire la complexité de vérification en modifiant significative le modèle et en proposant des blocks de spécification de propriétés linéaires basées sur les événements émis par le contrôleur. Le troisième article est dédié à la spécification de propriétés LTL en utilisant SLDV. Il propose des blocs Simulink configurables qui spécifient ces propriétés. Le but de ces blocs est de transformer les propriétés en assertions qui sont vérifiables par SLDV. La solution proposée dans le seconde et troisième article, est donc une extension de la bibliothèque de blocs de Simulink qui permet aux utilisateurs moins experts de spécifier et vérifier certaines propriétés LTL. Ce travail est donc limité aux propriétés LTL à temps discret, et restreint à certaines propriétés LTL. Nos travaux futurs consisteraient à l'extension de la bibliothèque de blocs de Simulink pour supporter des propriétés LTL plus complexes et à plus grande échelle.