Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent 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).

Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bug dans les logiciels (Evaluation Assurance Level, Safety Integrity Level). Elles sont utilisées dans le développement des 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.

Exemple

Comment vérifier que l'identité $(a b)^{2}=a^{2} b^{2} 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)^{2}$, puis $a^{2} b^{2} 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 ${\displaystyle }$ et l'$*$. Ici, les règles pourraient être:

• $\forall x,\ x^{2}=x*x\quad {\mathit {(R1)}}$
• $\forall x,y,z,\ x*(y z)=x*y x*z\quad {\mathit {(R2)}}$
• $\forall x,y,\ x*y=y*x\quad {\mathit {(R3)}}$
• $\forall x,\ x x=2x\quad {\mathit {(R4)}}$
• $\forall x,y,\ x y=y x\quad {\mathit {(R5)}}$

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

Démonstration

${\begin{aligned}(a b)^{2}&=(a b)*(a b)\quad {\mathit {(R1)}}\\&=(a b)*a (a b)*b\quad {\mathit {(R2)}}\\&=a*(a b) b*(a b)\quad {\mathit {(R3)}}\\&=a*a a*b b*a b*b\quad {\mathit {(R2)}}\\&=a^{2} a*b b*a b^{2}\quad {\mathit {(R1)}}\\&=a^{2} a*b a*b b^{2}\quad {\mathit {(R3)}}\\&=a^{2} 2(a*b) b^{2}\quad {\mathit {(R4)}}\\&=a^{2} b^{2} 2(a*b)\quad {\mathit {(R5)}}\\\end{aligned}}$

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

Catégories

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 typage des langages de programmation est historiquement une des premières méthodes formelles. Elle permet de restreindre des langages de programmes à des classes de programmes dont le comportement statique est assuré. Certes, les langages non-typés (tels que le lambda-calcul) permettent de grands pouvoirs d'expressivité, mais induisent des programmes sur lesquels il est plus difficilement possible de raisonner et dont la plupart des exécutions échouent (il n'est pas raisonnable d'additionner des chaînes de caractères) ;
• 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 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 vérification déductive (calcul de plus faible précondition, logique de séparation) consiste à donner une représentation purement logique et sémantique à un programme. Il s'agit alors de réduire le problème de la vérification des programmes à celui de démonstration de théorèmes de correction et de complétude. Ces théorèmes permettent de formaliser le comportement attendu (spécification) d'un programme et leur démonstration permet d'en affirmer leur vérité. Le raisonnement mathématique nécessaire à la preuve de théorèmes peut être assisté de logiciels d'assistants de preuve avec une aide (plus ou moins grande) de la machine (démonstration automatique).

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 (calcul d'invariant), etc.

Les méthodes formelles peuvent s'appliquer à différents stades 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.

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). Aujourd'hui, différents moyens permettent de formaliser la spécification des programmes, on parle alors de sémantique. Il en existe de différentes natures, chacune adaptée au paradigme de calcul voulu : dénotationnelle, opérationnelle, axiomatique, par machines à états finis...

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.

Vérification

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

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és 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, pour toute propriété, si cette 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.

Méthodes formelles ou semi-formelles

• Approche basée sur des états
  • Z
  • SAZ
  • Méthode B classique
  • ASM
  • TLA

• Approche basée sur des événements
  • Action Systems
  • Méthode B événementielle
  • VHDL
  • Esterel
  • SDL
  • LOTOS
  • E-LOTOS
  • EB3

• Approche basée sur les contrats
  • Eiffel

• Algébrique :
  • Larch : Larch family
  • CASL : Common Algebraic Specification Language

• Assistants de preuve :
  • Coq
  • Isabelle
  • Metamath

• Autres approches
  • Réseau de Petri
  • Algèbre de processus

Principaux outils

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

Bibliographie

• (en) Marie-Claude Gaudel, « Testing can be formal, too », Lecture Notes in Computer Science, vol. 915,‎ 1995, p. 82–96 (DOI 10.1007/3-540-59293-8_188, lire en ligne [PDF])
• Henri Habrias and Marc Frappier, Software Specification Methods, ISTE Ltd, 2006, (ISBN 1-905209-34-7).
• Jean-François Monin, Understanding Formal Methods, Springer, 2003, (ISBN 1-85233-247-6).

Annexes

Articles connexes

• Assistant de preuve
• Evaluation Assurance Level

Liens externes

• B Method.com : site consacré à la méthode B, méthode formelle avec preuve
• Le site international des méthodes formelles, voir [1]
• Le site de Formal Methods Europe, voir [2]