SPÉCIFICATION ET VÉRIFICATION DES SYSTÈMES EMBARQUÉS TEMPS RÉEL EN UTILISANT LA LOGIQUE DE RÉÉCRITURE

Abstract

Les systèmes embarqués temps réel doivent être correctement validés et vérifiés avant de les fabriquer et déployer afin d'augmenter leurs fiabilités et de réduire leurs coûts de maintenance. Les modèles sont utilisés depuis longtemps pour construire des systèmes complexes, dans pratiquement tous les domaines de l'ingénierie. C'est parce qu'ils fournissent une aide inestimable pour prendre des décisions de conception importantes avant la mise en oeuvre du système. Dans une activité classique d’Ingénierie Dirigée par les Modèles (IDM), les systèmes sont modélisés à l’aide d’une notation semi-formelle et sont par la suite validés puis implantés. L’étape de validation, basée sur ces modèles, est particulièrement cruciale pour les Systèmes Embarqués Temps-Réel (SETR), afin de s’assurer de leur bon fonctionnement. Cependant, une démarche IDM reste insuffisante dans le sens où elle n’indique pas comment utiliser les modèles pour appliquer l’analyse. Face à cette situation, l’intégration de méthodes formelles dans les cycles de développement de ces systèmes est devenue primordiale. Ces méthodes sont depuis longtemps reconnues afin d’aider au développement de systèmes fiables, en raison de leurs fondements mathématiques, réputés rigoureux sur l’exhaustivité de la vérification formelle qu’ils permettent de l’activer. Dans cette thèse, nous proposons une approche basée sur la transformation de modèle pour obtenir une spécification formelle de notre système, puis utilisons les techniques de vérification formelles pour prouver que la conception de tel système est correcte par rapport à sa spécification. Nous commençons par l’utilisation de diagramme d'états-transitions (Statechart), qui décrit un système temps réel, comme modèle source pour générer un code RT-Maude, ce code représente le module Maude du système temps réel (modèle cible). La deuxième partie de notre travail est de ; en se basant sur le module généré ; vérifier le système par rapport aux propriétés exprimées en logique temporelle linéaire (LTL) en utilisant Maude LTL Model- Checker. En outre, nous utilisons RT-Maude pour rechercher et analyser le système pour trouver des comportements indésirables. L'approche est illustrée à travers trois études de cas.