Méthode formelle (informatique)

Un article de Wikipédia, l'encyclopédie libre.

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 bogue dans les logiciels.

Ces techniques 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.

Sommaire

1 Exemple
2 Différentes techniques
3 Catégories
4 Spécification
5 Développement
6 Vérification
7 Preuves formelles
8 Quelques méthodes/langages de développement formel
9 Principaux outils
10 Voir aussi
11 Liens externes

[modifier] Exemple

Tout le monde connaît l'égalité $(a + b) 2 = a 2 + b 2 + 2 a b$ . 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 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. 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:

$\forall x, x^2 = x * x$
$\forall x,y,z, x * (y + z) = x*y + x*z$
$\forall x,y, x*y = y*x$
$\forall x, x + x = 2x$
$\forall x,y, x + y = y + x$

En se servant de ces règles et en partant de $(a + b) 2$ , on arrive facilement à trouver $a 2 + b 2 + 2 a b$ .

[modifier] 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), 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 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é. Or la plupart des problèmes de vérification formelle s'apparentent au problème de satisfaisabilité.

[modifier] 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 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.

[modifier] 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 terme 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).

[modifier] 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.

[modifier] 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».

[modifier] 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 ou 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épendant de la taille de l'espace des états, et peut donc s'appliquer sur des modèles avec un très grand nombre d'état, où même sur des modèles dont le nombre d'état 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 trouvent donc ses limites dans les ressources de l'ordinateur pour manipuler l'ensemble des états accessibles. Des techniques d'abstraction (éventuellement guidées par l'utilisateur) peuvent être utilisées pour améliorer l'efficacité des algorithmes.

[modifier] Quelques méthodes/langages de développement formel

Dites basées sur un modèle :
- VDM
- Z voir Notation Z
- B voir Méthode B
Algèbres de processus :
- CSP
- CCS
- Pi-calcul
Actions systems
Algébriques :
- Larch
- CASL
Synchrones :
- Signal, Lustre, Esterel
Mixtes
- LOTOS
- RAISE

[modifier] Principaux outils

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.