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

Les différentes approches de vérification fonctionnelles varient en fonction :

• de la nature du modèle à analyser ;

• de la nature des propriétés à vérifier.

• Nature du modèle à analyser. Le modèle peut être fini (par exemple, un protocole de cohérence de caches étudié pour un modèle à 5 caches) ou paramétré (le même protocole étudié pour un nombre n de caches, n étant un paramètre). Dans le premier cas l'ensemble des états accessibles du modèle est fini et on peut construire un algorithme qui les énumère. On se heurte à des problèmes d'explosion combinatoire de la taille de cet espace d'états. Dans le second cas, l'ensemble des états accessibles n'est pas borné et on ne peut pas définir un algorithme général qui parcourt automatiquement tous les états du système et permette de décider de la conformité des séquences du système par rapport à la spécification. On peut travailler sur des abstractions finies conservatives du modèle initial et retrouver des procédures de décision (donc automatisables) ou alors utiliser des méthodes de preuves manipulant les paramètres et requérant l'intervention de l'utilisateur pour guider la preuve lorsqu'il n'y a pas d'algorithme permettant de décider.

• Nature des propriétés à vérifier. On distingue deux grandes classes de propriétés :

  – les propriétés de sûreté qui indiquent qu'un mauvais fonctionnement n'arrivera jamais ;

  Exemples

  « La variable x ne peut jamais dépasser la valeur 10 ».

  « Deux processus concurrents voulant accéder à une ressource critique ne pourront jamais y accéder simultanément ».

  « Le...