Conception sûre de systèmes embarqués à base de COTS

• Main Author: Hajjar, Salam
• Language: ENG
• Published: INSA de Lyon 2013
• Subjects: [SPI:OTHER] Engineering Sciences/Other; [SPI:OTHER] Sciences de l'ingénieur/Autre; Automatique; Synthèse du control discret; Vérification formelle; Conception sure; Cots; Système embarqué
• Online Access: http://tel.archives-ouvertes.fr/tel-00952827; http://tel.archives-ouvertes.fr/docs/00/95/28/27/PDF/these.pdf

Le travail présenté dans ce mémoire concerne une méthode de conception sûre de systèmes(COTS). Un COTS est un composant matériel ou logiciel générique qui est naturellement conçu pour être réutilisable et cela se traduit par une forme de flexibilité dans la mise en oeuvre de sa fonctionnalité : en clair, une même fonction peut être réalisée par un ensemble (potentiellement infini) de scénarios différents, tous réalisables par le COTS. La complexité grandissante des fonctions implémentées fait que ces situations sont très difficiles à anticiper d'une part, et encore plus difficiles à éviter par un codage correct. Réaliser manuellement une fonction composite correcte sur un système de taille industrielle, s'avère être très coûteuse. Elle nécessite une connaissance approfondie du comportement des COTS assemblés. Or cette connaissance est souvent manquante, vu qu'il s'agit de composants acquis, ou développés par un tiers, et dont la documentation porte sur la description de leur fonction et non sur sa mise en IJuvre. Par ailleurs, il arrive souvent que la correction manuelle d'une faute engendre une ou plusieurs autres fautes, provoquant un cercle vicieux difficile à maîtriser. En plus, le fait de modifier le code d'un composant diminue l'avantage lié à sa réutilisation. C'est dans ce contexte que nous proposons l'utilisation de la technique de synthèse du contrôleur discret (SCD) pour générer automatiquement du code de contrôle commande correct par construction. Cette technique produit des composants, nommés contrôleurs, qui agissent en contraignant le comportement d'un (ou d'un assemblage de) COTS afin de garantir si possible la satisfaction d'une exigence fonctionnelle. La méthode que nous proposons possède plusieurs étapes de conception. La première étape concerne la formalisation des COTS et des propriété de sûreté et de vivacité (P) en modèles automate à états et/ou en logique temporelle. L'étape suivante concerne la vérification formelle du modèle d'un(des) COTS pour l'ensemble des propriétés (P). Cette étape découvrir les états de violation des propriétés (P) appelés états d'erreur. La troisième étape concerne la correction automatique des erreurs détectées en utilisant la technique SCD. Dans cette étape génère on génère un composant correcteur qui sera assemblé au(x) COTS original(aux) pour que leur comportement général respecte les propriétés souhaitées. L'étape suivante concerne la vérification du système contrôlé pour un ensemble de propriétés de vivacité pour assurer la passivité du contrôleur et la vivacité du système. En fin, une étape de simulation est proposée pour observer le comportement du système pour quelque scénarios intéressent par rapport à son implémentation finale.