Implantation matérielle de moniteurs pour la vérification en ligne des systèmes informatiques
Résumé
La vérification en ligne est une méthode de vérification qui consiste à vérifier un système pendant son exécution en lui intégrant un moniteur. Son rôle est d'observer l'exécution du système et de donner un verdict par rapport à une spécification voulue. La principale méthode d'implémentation de ces moniteurs consiste à les intégrer directement dans le code de l'application, on parle d'implémentation logicielle. Cependant, cela entraîne un surcoût de temps d'exécution. Les systèmes sur puces (SoC) intègrent sur un même composant un processeur et un circuit de logique programmable. Ce qui offre la possibilité d'implémenter un moniteur matériel dans le système. Cette solution permet de réduire le temps de surcoût d'exécution dû au dispositif de vérification en ligne. Cette présentation porte sur le travail réalisé lors d'un stage effectué à l'IRCCyN pour l'obtention du diplôme de master. Il est présenté une méthode d'implémentation matérielle de moniteur pour la vérification en ligne. Le système cible est un SoC intégrant un processeur et un circuit logique pouvant communiquer. L'application à vérifier s'exécute sur le processeur et le moniteur est implémenté sur le circuit logique. Le moniteur est généré à partir d'une propriété ptLTL qui traduit une spécification à vérifier.