Vérification formelle
Technique utilisée pour s'assurer qu'un système est conforme à sa spécification. Surtout (et presqu'exclusivement) employée dans les domaines de la micro-électronique et de la conception des logiciels.
La vérification formelle consiste soit à s'assurer que des propriétés spécifiques sont bien respectées par le système construit, soit à s'assurer que deux systèmes sont fonctionnellement équivalents. Contrairement à la vérification traditionnelle basée sur l'expérimentation, la vérification formelle est basée sur la démonstration logique ou mathématique.
| Sommaire |
Exemple
Tout le monde connaît l'égalité (a + b)2 = a2 + b2 + 2ab. Comment vérifier que cette égalité est juste ?
Par vérification traditionnelle, il faudrait prendre toutes les valeurs possibles de a, les croiser avec toutes les valeurs possibles de b, et pour chaqe couple, calculer (a + b)2, puis a2 + b2 + 2ab, et s'assurer que l'on obtient le même résultat. Bien entendu, si les domaines de a et de b sont grands, cette vérification peut être très longue. Et si les domaines sont infinis (par exemple les réels), cette vérification est infinie.
Par vérification formelle, on n'utilise que des valeurs symboliques et on applique des règles connues. Ici, les règles connues seraient:
En se servant de ces règles et en partant de (a + b)2, on arrive facilement à trouver a2 + b2 + 2ab.
Différentes techniques
La vérification comprend plusieurs techniques, souvent complémentaires.
- La démonstration de théorèmes est une technique souvent peu automatisée qui consiste à réécrire des formules en utilisant un ensemble de règles connues ainsi que l'induction.
- Les BDDs (pour Binary Decision Diagrams, [1] sont des représentations de formules Booléennes. Les BDDs ont l'avantage d'être parfois exponentiellement plus compactes que les formules explicites qu'ils représentent. Ils sont de plus canoniques. Cette représentation est surtout utilisée pour la vérification formelle appliquée aux circuits digitaux.
- SAT [2] est un terme plutôt général pour désigner un ensemble de méthodes visant à résoudre le problème de satisfaisabilité. Or la plupart des problèmes de vérification formelle s'apparentent au problème de satisfaisabilité.
Principaux outils
Seuls les principaux outils de vérification formelle non commerciaux sont listés ci-dessous.
- Coq: assistant d'aide à la preuve (ie, formalisation de preuves et démonstration semi-automatisée).
- PVS: assistant d'aide à la preuve.
- ACL2: démonstration de théorèmes automatisée.
- SMV, nuSMV: démonstration de propriétés avec BDDs et SAT.
- zChaff: démonstration avec SAT.
- Murφ: démonstration de propriétés.
Voir aussi
- Méthode formelle (informatique)
- Spécification
- Preuves formelles