Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin de démontrer leur validité par rapport à une certaine spécification.

Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bug dans les logiciels, c'est-à-dire d'acquérir des niveaux d'évaluation d'assurance élevés, elles sont basées sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou parfois, son code objet). Cependant, elles sont généralement coûteuses en ressources (humaines et matérielles) et actuellement réservées aux logiciels les plus critiques. Leur amélioration et l'élargissement de leurs champs d'application pratique sont la motivation de nombreuses recherches scientifiques en informatique.

Comment vérifier que l' identité (a + b) = a + b + 2(a * b) est correcte ?

Une vérification naïve pourrait consister à examiner toutes les valeurs possibles de a, à les croiser avec toutes les valeurs possibles de b et, pour chaque couple, à calculer (a + b), puis a + b + 2(a * b) et à s'assurer que l'on obtient le même résultat. 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 ne peut pas être exhaustive.

En vérification formelle, on utilise des valeurs symboliques et on applique les règles qui régissent le + et l' * . Ici, les règles pourraient être:

• $\forall x,x^2=x\ast x$
• $\forall x,y,z,x\ast (y+z)=xy+xz$
• $\forall x,y,xy=yx$
• $\forall x,x+x=2x$
• $\forall x,y,x+y=y+x$

En se servant de ces règles, on arrive à montrer que (a + b) = a + b + 2(a * b).

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é.

Différents corpus mathématiques ont été utilisés pour élaborer des raisonnements formels sur les logiciels. Cette diversité d'approche a engendré des «familles» de méthodes formelles. Citons notamment («Les méthodes basées sur ...» ):

• Le model checking analyse exhaustivement l'évolution du système lors de ses exécutions possibles. Par exemple, pour démontrer l'absence d'erreurs à l'exécution, on pourra tester l'absence d'états d'erreur dans l'ensemble des états accessibles du système. Il s'agit alors d'une forme de test (informatique) exhaustif, mais mené à l'aide d'algorithmes astucieux permettant d'énumérer les états du système sous une forme symbolique économique. En général, il n'est pas possible d'analyser directement le système, mais on en analyse plutôt un modèle informatique, plus ou moins abstrait par rapport à la réalité (voir aussi interprétation abstraite). Dans les évolutions récentes du software model-checking, l'analyseur peut automatiquement enrichir le modèle pour en obtenir un moins abstrait; des preuves peuvent être fournies après des itérations de ce processus, qui peut ne pas converger.

• L'analyse statique par interprétation abstraite, schématiquement, calcule symboliquement un sur-ensemble des états accessibles du système.

• La preuve automatique de théorème tend à démontrer automatiquement des théorèmes sur les formules logiques décrivant la sémantique du programme.

• Les assistants de preuve permettent à l'utilisateur de démontrer des théorèmes sur le programme, avec une aide (plus ou moins grande) et une vérification par la machine.

Il existe des gradations et des mélanges possibles entre ces méthodes. Par exemple, un assistant de preuve pourra être suffisamment automatisé pour prouver automatiquement la plupart des lemmes utilitaires d'une preuve de programmes. Un model-checker pourra être appliqué sur un modèle construit à l'aide d'un prouveur automatique de théorèmes. Une interprétation abstraite préalable pourra limiter le nombre de cas à démontrer dans une preuve de théorèmes, etc.

Les méthodes formelles peuvent s'appliquer à différent stade du processus de développement d'un système (logiciel, électronique, mixte), de la spécification jusqu'à la réalisation finale. Voir l'exemple de la méthode B.

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).

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.

Une spécification peut être utilisée comme base pour prouver des propriétés sur le système. La spécification est le plus souvent une représentation abstraite (avec moins de détails) du système en développement: débarrassé de détails encombrants, il est en général plus simple de prouver des propriétés sur la spécification que directement sur la description complète et concrète du système.

Certaines méthodes, comme la Méthode B, s'appuient sur ce principe: le système est modélisé à plusieurs niveaux d'abstraction, en partant du plus abstrait et en allant au plus concret (ce processus est appelé « raffinement » puisqu'il ajoute des détails au fur et à mesure); la méthodologie assure que toutes les propriétés prouvées sur les modèles abstraits sont conservées sur les modèles concrets. Cette garantie est apportée par un ensemble de preuves dites «de raffinement».

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.

• Approche basée sur des états

• Z voir Notation Z

• SAZ

• Méthode B classique voir Méthode B

• ASM

• TLA+

• Approche basée sur des événements

• Action Systems

• Méthode B événementielle voir Méthode B

• VHDL

• Esterel

• SDL

• LOTOS

• E-LOTOS

• EB3

• Algébriques :

• Larch :Larch family

• CASL : Common Algebraic Specification Language

• Autre approche

• Coq (logiciel)

• Réseau de Petri

• Algèbre de processus

• ACL2 : démonstration de théorèmes automatisée.
• AtelierB : spécification et preuve avec la méthode B.
• CADP : construction et analyse de processus distribués
• Coq : assistant d'aide à la preuve (c'est-à-dire formalisation de preuves et démonstration semi-automatisée).
• Murφ : démonstration de propriétés.
• Prototype Verification System : assistant d'aide à la preuve.
• SMV, nuSMV : démonstration de propriétés avec BDDs et SAT.
• zChaff : démonstration avec SAT.