Méthode formelle (informatique) - Définition

Différentes approches

La vérification comprend plusieurs approches, souvent complémentaires.

• La démonstration de théorèmes est une approche qui tend à être de plus en plus automatisée et assistée par ordinateur. Elle consiste à énoncer des propositions et à les démontrer dans un système de déduction de la logique mathématique, en particulier dans le calcul des prédicats.
• Les BDDs (pour Binary Decision Diagrams), sont des représentations de formules Booléennes qui ont l'avantage d'être parfois exponentiellement plus compactes que les formules explicites qu'ils représentent. Cette représentation est surtout utilisée pour la vérification formelle appliquée aux circuits numériques.
• SAT est un terme plutôt général pour désigner un ensemble de méthodes visant à résoudre le problème de satisfaisabilité.

Développement

Une fois qu'une spécification a été développée, elle peut être utilisée comme référence pendant le développement du système concret (mise au point des algorithmes, réalisation en logiciel et/ou circuit électronique). Par exemple:

• Si la spécification formelle est dotée d'une sémantique opérationnelle, le comportement observé du système concret peut être comparé avec le comportement de la spécification (qui elle-même doit être exécutable ou simulable). De plus, une telle spécification peut faire l'objet d'une traduction automatique vers le langage cible.
• Si la spécification formelle est dotée d'une sémantique axiomatique, les préconditions et postconditions de la spécification peuvent devenir des assertions dans le code exécutable. Ces assertions peuvent être utilisées pour vérifier le fonctionnement correct du système pendant son exécution (ou simulation), ou mieux encore des méthodes statiques (preuve de théorème, model-checking) peuvent être utilisées pour vérifier que ces assertions seront satisfaites pour toute exécution du système.

Spécification

Les méthodes formelles peuvent être utilisées pour donner une spécification du système que l'on souhaite développer, au niveau de détails désiré. Une spécification formelle du système est basée sur un langage formel dont la sémantique est bien définie (contrairement à une spécification en langage naturel qui peut donner lieu à différentes interprétations). Cette description formelle du système peut être utilisée comme référence pendant le développement. De plus, elle peut être utilisée pour vérifier (formellement) que la réalisation finale du système (décrite dans un langage informatique dédié) respecte les attentes initiales (notamment en termes de fonctionnalité).

La nécessité des méthodes formelles s'est fait sentir depuis longtemps. Dans le rapport Algol 60, John Backus présentait une notation formelle pour décrire la syntaxe des langages de programmation (notation appelée Backus-Naur form, BNF).

Preuves formelles

Les méthodes formelles prennent tout leur intérêt lorsque les preuves elles-mêmes sont garanties correctes formellement. On peut distinguer deux grandes catégories d'outils permettant la preuve de propriété sur des modèles formels:

• La preuve automatique de théorème, qui consiste à laisser l'ordinateur prouver les propriétés automatiquement, étant donnés une description du système, un ensemble d'axiomes et un ensemble de règles d'inférences. Cependant la recherche de preuve est connue pour être un problème non décidable en général (en logique classique), c'est-à-dire que l'on sait qu'il n'existe (et n'existera jamais) aucun algorithme permettant de décider en temps fini si une propriété est vraie ou fausse. Il existe des cas où le problème est décidable (fragment gardé de la logique du premier ordre par exemple) et où des algorithmes peuvent donc être appliqués. Cependant même dans ces cas, le temps et les ressources nécessaires pour que les propriétés soient vérifiées peut dépasser des temps acceptables ou les ressources dont dispose l'ordinateur. Dans ce cas il existe des outils interactifs qui permettent à l'utilisateur de guider la preuve. La preuve de théorème, par rapport au model-checking, a l'avantage d'être indépendante de la taille de l'espace des états, et peut donc s'appliquer sur des modèles avec un très grand nombre d'états, ou même sur des modèles dont le nombre d'états n'est pas déterminé (modèles génériques).
• Le model checking, qui consiste à vérifier des propriétés par une énumération exhaustive et astucieuse (selon les algorithmes) des états accessibles. L'efficacité de cette technique dépend en général de la taille de l'espace des états accessibles et trouve donc ses limites dans les ressources de l'ordinateur pour manipuler l'ensemble des états accessibles. Des techniques d'abstractions (éventuellement guidées par l'utilisateur) peuvent être utilisées pour améliorer l'efficacité des algorithmes.