Page d'accueil	encyclopedie-enligne.com en page d'accueil
Liste Articles: [0-A] [A-C] [C-F] [F-J] [J-M] [M-P] [P-S] [S-Z] | Liste Catégories | Une page au hasard | Pages liées

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