Colloque

Une approche hiérarchique à la vérification formelle des systèmes embarqués en utilisant MDGs

S. Balakrishnan

S. Tahar

Membre a labase

S. Balakrishnan

Résumé du colloque

En cet article, on propose une approche hiérarchique pour la modélisation et la vérification formelle d’un système embarqué complet à des niveaux élevés d’abstraction, en utilisant les graphes de décision MDG (Multiway Decision Graphs). L’approche est sur une application de contrôleur de souris roulant sur un microcontrôleur commercial (PIC 16C71). Le système est modélisé à différents niveaux de la hiérarchie de conception c.-à-d., le niveau matériel du microcontrôleur, l’architecture de jeux d’instruction du microcontrôleur (ISA), le niveau de code assembleur de logiciel embarqué et la spécification de comportement du logiciel. L’exactitude de la plateforme matérielle d’assembleur de l’architecture destinée est établie en vérifiant l’équivalence entre le matériel RTL et l’ISA, en utilisant l’outil de vérification d’équivalence de MDG. L’étape suivante est de vérifier l’application particulière embarquée dans le système en vérifiant l’équivalence entre le code d’assembleur et son comportement destiné, indiqués comme organigramme. Davantage de vérification est faite sur différents niveaux d’abstraction du système par la vérification de propriété avec les outils de vérification de modèles de MDG. Des incohérences dans le code d’assembleur du logiciel embarqué comme édité dans les notes d’application du constructeur, ont été découvertes par vérification d’équivalence et vérification de propriété. Etant donné la consommation relativement petite de temps de CPU et de mémoire dans les expériences réalisées, l’approche de vérification adoptée démontre l’efficacité de l’utilisation des types abstraits de données et des fonctions non-interprétées dans MDGs pour contenir les complexités inhérentes d’un système embarqué entier de façon automatisé.