التفاصيل البيبلوغرافية
| العنوان: |
Conception sûre de systèmes embarqués à base de COTS ; Safe design method of embedded systems based on COTS |
| المؤلفون: |
Hajjar, Salam |
| المساهمون: |
Lyon, INSA, Niel, Eric |
| سنة النشر: |
2013 |
| المجموعة: |
theses.fr |
| مصطلحات موضوعية: |
Automatique, Synthèse du control discret, Vérification formelle, Conception sure, Cots, Système embarqué, Automatics, Discrete controller synthesis, Model checking, Safe design, Embedded System, 629.807 2 |
| الوصف: |
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 ... |
| نوع الوثيقة: |
thesis |
| اللغة: |
English |
| Relation: |
http://www.theses.fr/2013ISAL0064/document |
| الاتاحة: |
http://www.theses.fr/2013ISAL0064/document |
| Rights: |
Open Access ; http://purl.org/eprint/accessRights/OpenAccess |
| رقم الانضمام: |
edsbas.F7F4D319 |
| قاعدة البيانات: |
BASE |