Méthodes formelles pour la vérification des systèmes embarqués

Les systèmes embarqués sont soumis à de nombreuses contraintes et certains sont en interaction étroite avec des procédés dangereux ou interviennent dans des processus de décisions impactant des vies humaines. Le développement de tels systèmes doit offrir des garanties de bon fonctionnement et de bon rétablissement en cas de défaillance d'une partie interne ou d'un environnement non prévu.

Des méthodes de vérifications formelles peuvent être mises en œuvre pour augmenter le degré de confiance des systèmes. Trois grandes classes se distinguent :

• la preuve assistée ( theorem-proving ) ;

• la vérification par modèle ( model-checking ) et ses nombreuses variantes et extensions ;

  enfin le raffinement de spécification.

On présente le positionnement de ces approches dans le flot de conception des systèmes embarqués.

Pour chaque approche, on s'attache à présenter simplement le principe de base, le domaine applicatif principal, les outils disponibles ainsi que les réalisations académiques et industrielles. Cet article n'utilise pas de formalisme mathématique poussé pour être accessible au plus grand nombre. Les références bibliographiques permettent d'approfondir chaque approche tant sur les aspects formels que sur les outils disponibles ou (le cas échéant) leur utilisation dans un contexte industriel.