Méthode formelle (informatique)
En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement sur des programmes informatiques, ou aussi des matériels électroniques, afin de démontrer leur correction, en se basant sur des raisonnements de logique mathématique.
Ces méthodes permettent d'obtenir une très forte assurance de l'absence de bogue dans les logiciels. 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.
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).
Citons notamment :
- 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, 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 Méthode B
| Sommaire |
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 fonctionalité).
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 normal form, BNF).
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ée pour vérifier le fonctionnement correcte 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ée pour vérifier que ces assertions seront satisfaites pour tout 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 encombrant, 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 toute propriété prouvée sur le modèles abstraits sont conservées sur les modèles concrets (il n'est pas nécessaire de refaire les preuves). ha
Preuves formelles
Les méthodes formelles prennent tout leur intérêt lorsque les preuves elles-mêmes sont garanties correcte 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écidables (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 où 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 de états accessibles. Des techniques d'abstraction (éventuellement guidées par l'utilisateur) peuvent être utilisée pour améliorer l'efficacité des algorithmes.
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
- Actions systems
- Algébriques :
- Larch
- CASL
- Synchrones :
- Signal, Lustre
- Mixtes
- Lotos
- RAISE
Le site international des méthodes formelles, voir [1] Le site de Formal Methods Europe, voir [2]
Voir aussi
- vérification formelle : discipline des sciences de l'information spécialisée dans la preuve logicielle.