Implémentation d’un mécanisme de Vérification en Ligne sur un SoPC 

Télécharger le fichier pdf d’un mémoire de fin d’études

Architecture des systèmes informatiques pour l’embarqué

L’architecture de base d’un système informatique est représentée sur la Figure 1.2. Elle se compose d’un ou plusieurs processeurs qui exécutent le code de du programme, de mémoires qui stockent le code et les données du programme, et de multiples périphériques.
Ces éléments communiquent entres eux à travers des bus de communication.
La conception d’un système informatique peut se faire de différentes façons [17] :
— Par l’assemblage des différents éléments. De cette façon il possible de concevoir un système informatique au plus proche des besoins réels. Cependant cette approche requiert un temps de développement relativement long.
— Par l’utilisation d’un microcontrôleur qui intègre les ressources de bases (un pro-cesseur, de la mémoire et les périphériques de base) nécessaires au développement d’un système informatique.
— Par l’utilisation d’un système sur puce (SoC pour system on a chip) qui intègre tous les éléments nécessaires à la conception d’un système informatique : un ou plusieurs processeurs, de la mémoire, de multiples périphériques d’interfaces et même des capteurs. L’utilisation de SoCs permet de faciliter grandement le temps de développement d’un système informatique.

Les systèmes temps réel

Un système est qualifié de « temps réel » quand il est capable de contrôler un pro-cédé physique à une vitesse adaptée par la prise en compte d’un ensemble d’exigences temporelles.
Selon l’importance des exigences temporelles à respecter, un système temps réel peut être qualifié de strict ou souple :
— Le temps réel strict qualifie les systèmes qui doivent impérativement respecter toutes leurs échéances. Ces systèmes sont généralement intégrés dans en environnement critique où la violation d’une exigence temporelle peut avoir des conséquences dramatiques.
— Le temps réel souple qualifie les systèmes qui peuvent se permettre de violer cer-taines échéances. Ces systèmes sont, par exemple, présents dans le domaine du multimédia où une violation de propriété peut avoir des conséquences sur la qua-lité du service rendu.
Une application temps réel se compose de tâches, qui sont des séries d’actions à exé-cuter, qui doivent être ordonnancés par le système de façon à respecter leur priorité et leur date d’échéance. Ces tâches peuvent être :

— Périodiques, si elles doivent s’exécuter à intervalle régulier.
— Sporadiques, si elles peuvent s’exécuter à n’importe quel moment mais où il est possible de définir un temps minimal entre deux activation. Lors de l’étude de l’ordonnancement, il est souvent commode de se ramener à un modèle de tâche périodique.
— Apériodiques, si elles peuvent s’exécuter à n’importe quel moment sans pouvoir définir un temps minimal entre deux activations. Avec ce type de tâche, il impossible de garantir un ordonnancement.
On représente généralement une tâche périodique à travers le tuple r0, P, C, D où :
— r0 correspond à la date de réveil de la première instance de la tâche ;
— P correspond à la période de la tâche ;
— C correspond à la durée d’exécution de la tâche (le pire cas) ;
— D correspond au délai critique de la tâche, c’est à dire le temps maximum accepté entre le réveil d’une instance de tâche et sa terminaison.
Sur la Figure 1.3, on retrouve deux instances de tâche où ri correspond à la date de réveil de la ième instance de la tâche et di correspond à la date d’échéance du ième instance. La première instance s’exécute sans être préemptée. La deuxième instance est préemptée et dépasse son échéance, ce qui dans le cas d’une tâche critique est une violation des exigences temporelles.
D’un point de vue logiciel, plusieurs architectures sont envisageables pour construire une application temps réel.

Les aspects de la sûreté de fonctionnement abordés dans nos travaux

Les systèmes qui nous intéressent, sont souvent critiques et nécessitent un niveau de fiabilité élevé. Les attributs de la sûreté de fonctionnement qui les caractérisent sont la fiabilité et la sécurité-innocuité.
Les fautes que l’on considère dans nos travaux sont les fautes transitoires qui peuvent provoquer des erreurs logicielles. Pour ce prémunir de ces fautes deux méthodes sont possibles :
1. L’utilisation de composants durcis qui permettent de se prémunir des SEEs.
2. L’utilisation de mécanismes de tolérance aux « fautes » afin de détecter les erreurs issues des SEEs.
La première méthode étant trop coûteuse, nous aborderons dans cette thèse le dévelop-pement d’un mécanisme de tolérance aux fautes.

Les mécanismes de tolérance aux fautes

Architecture d’un mécanisme de tolérance aux fautes

Comme présenté sur la Figure 1.6, un mécanisme de tolérance aux fautes se compose de deux composants :
— Un mécanisme de détection dont le rôle est de détecter quand une faute ou une erreur apparaît sur le système au plus tôt, c’est-à-dire avant que celle-ci ne se fautes propage.
— Un mécanisme de rétablissement qui, quand une erreur est détectée par un mé-canisme de détection, rétablit le système afin qu’il soit toujours opérationnel. Ce mécanisme peut être implémenté selon trois approches possibles :
— La reprise qui consiste à sauvegarder périodiquement l’état du système et de le ramener à l’état de la dernière sauvegarde lors d’une détection d’erreur.
— La poursuite qui consiste à continuer l’exécution du système en le forçant à poursuivre dans un mode dégradé.

— La compensation qui consiste à utiliser la redondance du système quand elle existe pour masquer les erreurs.
La mise en œuvre d’une approche de rétablissement est particulièrement dépendante de l’application visée. Ainsi dans la suite nous nous focaliserons sur les mécanismes de détection.

Panorama des mécanismes de détection

Un mécanisme de détection peut être implémenté dans le système soit au niveau matériel soit au niveau logiciel. Les deux approches sont caractérisées par leur efficacité et leur coût. L’efficacité s’exprime par classes de fautes couvert par le mécanisme et par la latence de détection. Le coût désigne les ressources (surface du silicium, empreinte mémoire, surcoût temporel) utilisés pour l’implémentation du dispositif. Ces mécanismes sont soit basés sur de la redondance, soit sur du contrôle de cohérence.

Mécanismes basés sur la redondance

La duplication
La duplication est l’un des moyens de détection les plus utilisés en raison de sa simpli-cité. Le principe est de réaliser plusieurs fois la même fonction et de comparer les résultats.
La duplication peut se faire de façon spatiale ou temporelle, et peut être appliquée aux différents niveaux d’un système.
L’approche spatiale consiste à faire réaliser un même calcul simultanément par plu-sieurs sous-systèmes. Ces sous-systèmes peuvent être identiques si l’on cherche à détecter des erreurs physiques internes, ou différentes si l’objectif est de détecter des fautes de conception. Comme les calculs sont effectués en parallèle, le surcoût temporel est géné-ralement faible. Par contre, en ce qui concerne l’utilisation des ressources, celle-ci est au minimum doublé.

L’approche temporelle consiste à faire exécuter plusieurs fois la même opération par un composant (matériel ou logiciel) et de comparer ensuite le résultat de ces différentes exécutions. Cette approche ne nécessite aucune ressource matérielle supplémentaire (sauf pour le comparateur) mais ajoute un surcoût temporel qui est au minimum doublé. Aussi, cette approche ne permet pas de détecter des changements d’état de la mémoire qui ont eu lieu avant l’exécution de l’opération.
La redondance d’information
La redondance d’information consiste à dupliquer une information ou à lui ajouter des bits de contrôles qui sont calculés par un code détecteur d’erreurs voir un code correcteur d’erreurs. Les approches basées sur la redondance d’information permettent de détecter les erreurs dues à une faute pendant la transmission d’une information ou d’une faute physique au niveau de la mémoire stockant cette information. L’impact de cette approche est l’augmentation de l’empreinte mémoire ainsi qu’une augmentation du surcoût temporel dû au temps de la comparaison et des accès mémoires.

Les mécanismes basés sur du contrôle de cohérence

Le contrôle de cohérence regroupe les mécanismes permettant de vérifier que l’exé-cution du système est cohérente vis-à-vis d’un certain nombre de spécifications. Ces mé-thodes permettent généralement de détecter un large spectre de fautes avec un faible coût. Par contre le taux de couverture est généralement faible en comparaison des mé-thodes précédemment présentées. On peut distinguer 4 types de contrôle de cohérence qui sont : le contrôle de données, le contrôle temporel, le contrôle d’exécution le contrôle de vraisemblance.

Les mécanismes de tolérance aux fautes

Le contrôle de données
Cela consiste à ajouter du code spécifique dans un programme afin de vérifier l’in-tégrité des données. Cela peut par exemple être utilisé pour vérifier qu’une valeur est bien comprise dans un intervalle de valeurs possibles ou encore que l’écart entre la valeur courante et précédente d’une donnée est cohérente.
Le contrôle temporel
Cela permet d’assurer que les différents composants matériels et logiciels d’un sys-tème sont toujours en vie. Cela passe par l’utilisation de watchdog qui sont des timers devant être rafraîchis soit avant le dépassement d’une échéance, soit à une fréquence fixe. Si le temps est dépassé, un signal d’erreur est généré, celui-ci conduit généralement au redémarrage du système.
Contrôle d’exécution
Le contrôle d’exécution permet de vérifier le flot de contrôle de programmes exécutés, c’est-à-dire que les instructions du programme sont lues correctement et dans le bon ordre. Le contrôle d’exécution peut se faire au niveau des instructions machines ou à des niveaux d’abstractions plus élevés comme au niveau des blocs d’instruction, des fonctions, ou encore en faisant évoluer un modèle abstrait du système.

Contrôle de vraisemblance
Le contrôle de vraisemblance consiste à vérifier la cohérence des différents éléments d’un programme par l’utilisation de matériels ou logiciels spécifiques.
Les exceptions sont des interruptions générées par la détection de conditions excep-tionnelles (erreurs) pendant l’exécution d’un programme par des mécanismes matériels présents dans les processeurs. Ces conditions exceptionnelles peuvent porter sur des er-reurs au niveau de l’utilisation des bus (accès à une région mémoire invalide, transfert d’une donnée dont la taille n’est pas supportée par le périphérique ciblé, etc.) ou encore de l’exécution d’une instruction (division par zéro, exécution d’une instruction non-définie, etc.).

Langages formels pour la spécification de pro- priétés

Les principales catégories de langages de spécifications

Pour exprimer une propriété à vérifier, plusieurs langages peuvent être utilisés. Ces langages peuvent  être classés en trois catégories [9] qui sont :
Les logiques temporelles linéaires [42] qui permettent d’exprimer des propriétés à vérifier sous la forme de formules logiques. Ces logiques sont des logiques modales dont les modalités donnent des informations sur l’écoulement du temps.
Les expressions régulières [54] sont des expressions composées de propositions ato-miques et d’opérateurs qui permettent de définir les mots, acceptés par une spé-cification. Une expression régulière décrit donc un langage rationnel qui peut être reconnu par un automate à états finis (théorème de Kleene [28]).

Les machines d’état permettent d’exprimer des propriétés qui sont directement vé-rifiables. En effet la synthèse d’un moniteur à partir d’une formule de logique tem-porelle [11] ou d’une expression régulière est souvent réalisée sous la forme d’une machine d’état. Cependant il est généralement difficile d’exprimer directement une propriété sous la forme d’une machine d’état.
Pour manipuler les formalismes mathématiques listés ci-dessus, des langages de spé-cification ont été définis. Dans le cadre qui nous intéresse dans ce manuscrit, on citera par exemple le langage standardisé PSL (Property Specification Language) [43, 14, 37], ou encore la logique EAGLE [8, 20] qui incluent les opérateurs des logiques temporelles et des expressions régulières.

Panorama des logiques temporelles linéaires

Une logique temporelle est linéaire quand elle permet d’exprimer des propriétés por-tant sur des chemins individuels, donc sur une exécution. Les logiques linéaires s’opposent aux logiques arborescentes qui permettent d’exprimer des propriétés sur des arbres d’exé-cution. Comme dans le domaine de la vérification en ligne, on s’intéresse à l’évaluation de la satisfaction d’une trace d’exécution par rapport à une propriété, seules les logiques linéaires sont considérées.

On retrouve dans la littérature plusieurs logiques linéaires qui, selon leurs caractéris-tiques, vont avoir un pouvoir d’expressivité différent. Les deux principales caractéristiques de ces logiques sont :
— Les types de modalités temporelles qu’elles utilisent. Celles-ci peuvent faire référence au futur comme la logique LTL (Linear Temporal Logic) ou au passé comme la logique ptLTL (past time Linear Temporal Logic).
— La notion du temps qui peut être simplement qualitatif comme pour les logiques précédemment citées, ou quantitatif comme pour les logiques TLTL [11, 10] et MTL [61] qui étendent LTL, et la logique ptMTL [45] qui étend sur ptLTL.
Dans le cadre de nos travaux, on se restreindra à l’utilisation d’une logique temporelle non-temporisée. Comme on le verra dans la suite, les propriétés que l’on cherche à exprimer porteront sur l’exécution du code d’un SETR où il n’y a pas de notion de temps quantitatif.

Comparaison des logiques LTL et ptLTL

Comme toute logique modale, LTL et ptLTL sont construites à partir d’un ensemble fini de propositions atomiques (noté AP ), des opérateurs de la logique propositionnelle (non : ¬ , et : ∧, ou : ∨, implique : → ) et d’opérateurs temporels.
La logique LTL
Une formule LTL ϕ est définie syntaxiquement de la façon suivant : ϕ = p ∈ AP S ¬ϕ S ϕ ∨ ϕ S Zϕ S ϕ S nϕ S ϕ1Uϕ2 S
Où p désigne une proposition atomique et ϕ, ϕ1 et ϕ2 des formules LTL. La signification des opérateurs temporels est présentée ci-dessous :
F Suivant F est vraie à l’instant suivant
ZF Toujours F est toujours vraie
F Fatalement F sera vraie
n1 UF 2 Jusqu’à F1 est vraie jusqu’à ce que F2 devienne vraie
La satisfaction d’une formule LTL est évaluée sur l’ensemble B2 = {⊤, ⊥} (où ⊤ signifie que la formule est vérifiée et ⊥ signifie que la formule n’est pas vérifiée) et à partir d’une trace qui est constituée d’une séquence infinie de propositions atomiques. Notons σ = s0s1 .

Table des matières

Introduction générale 9
1 Sûreté de fonctionnement des systèmes embarqués temps réel 
1.1 Les systèmes embarqués temps réel
1.1.1 Définition et caractérisation d’un système embarqué
1.1.2 Architecture des systèmes informatiques pour l’embarqué
1.1.3 Les systèmes temps réel
1.2 Le principe de la sûreté de fonctionnement
1.2.1 Définition et typologie
1.2.2 Classification et origines des fautes
1.2.3 Les aspects de la sûreté de fonctionnement abordés dans nos travaux
1.3 Les mécanismes de tolérance aux fautes
1.3.1 Architecture d’un mécanisme de tolérance aux fautes
1.3.2 Panorama des mécanismes de détection
1.3.3 Mécanismes basés sur la redondance
1.3.4 Les mécanismes basés sur du contrôle de cohérence
1.4 Système d’exploitation temps réel robuste
1.4.1 Le rôle d’un SETR dans la sûreté de fonctionnement
1.4.2 Classification des erreurs transitoires dans une application multitâche temps réel
1.4.3 Exemple de SETR robuste
1.5 Conclusion : Positionnement des travaux de la thèse
2 La vérification en ligne 
2.1 Introduction à la vérification en ligne
2.1.1 Le principe de fonctionnement
2.1.2 Positionnement de la vérification en ligne
2.2 Langages formels pour la spécification de propriétés
2.2.1 Les principales catégories de langages de spécifications
2.2.2 Panorama des logiques temporelles linéaires
2.2.3 Comparaison des logiques LTL et ptLTL
2.3 Synthèse de moniteur
2.3.1 La synthèse sous la forme d’une machine d’état
2.3.2 La synthèse sous la forme d’un circuit
2.4 L’implémentation d’un mécanisme de vérification en ligne
2.4.1 L’implémentation logicielle
2.4.2 L’implémentation matérielle
2.5 Conclusion : Approche suivie dans la thèse
3 Implémentation d’un mécanisme de Vérification en Ligne sur un SoPC 
3.1 Introduction
3.2 Génération d’un circuit logique pour la vérification d’une formule ptLTL
3.2.1 Architecture du circuit de vérification d’une formule ptLTL
3.2.2 Outil de synthèse des circuits de vérification
3.3 Présentation de l’architecture du mécanisme de vérification en ligne
3.3.1 Architecture générale du système
3.3.2 Observation du programme à vérifier
3.3.3 Architecture du dispositif matériel de vérification en ligne
3.3.4 Synchronisation de l’architecture
3.3.5 Durcissement du mécanisme de détection
3.4 Conclusion
4 Cas d’étude : La surveillance du SETR Trampoline 
4.1 Le système d’exploitation temps réel Trampoline
4.1.1 Présentation de Trampoline
4.1.2 Description des structures de données internes
4.1.3 Flot d’exécution d’un appel de service
4.2 Spécification des propriétés à vérifier
4.2.1 Le principe de la surveillance du noyau de Trampoline
4.2.2 Surveillance de l’exécution du System Call Handler
4.2.3 Surveillance des appels de fonctions
4.2.4 Surveillance des structures internes
4.2.5 Synthèse des propriétés spécifiées
4.3 Mise en œuvre de la surveillance de Trampoline
4.3.1 Instrumentation de Trampoline
4.3.2 Génération du circuit du dispositif de vérification
4.3.3 Évaluation du coût de mise en œuvre du dispositif de vérification
4.4 Conclusion
5 Évaluation par injection de fautes 
5.1 Présentation du processus d’injection de fautes
5.1.1 Contexte et objectif
5.1.2 Développement d’une plateforme d’injection de fautes
5.1.3 Sélection de la liste des fautes à injecter
5.1.4 Description du processus d’injection de fautes
5.2 Développement d’une application de référence
5.2.1 Description de l’application
5.2.2 Récupération des résultats
5.2.3 Caractéristiques de l’application
5.3 Analyse de la campagne d’injection de fautes
5.3.1 Classification de l’impact des fautes
5.3.2 Évaluation du taux de détection d’erreur par le mécanisme de vérification en ligne
5.3.3 Analyse des fautes non-détectées
5.4 Conclusion
Conclusion générale et perspectives 
A Utilisation de ptLTL dans le cadre de la thèse 
A.1 Les opérateurs ptLTL
A.2 Illustration par un exemple
B Spécification des propriétés de Trampoline 
B.1 Surveillance des appels de fonctions
B.2 La surveillance de l’exécution du System Call Handler
B.2.1 Rappel sur le code du System Call Handler
B.2.2 Propriétés d’imbrication
B.2.3 Propriétés d’ordre
B.2.4 Propriétés relatives à la structure tpl_kern
B.3 Surveillance des structures internes
Bibliographie 

Télécharger le rapport complet