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

Analyse statique de programmes

En informatique, l'analyse statique de programmes est une famille de techniques permettant de dériver des résultats sur l'exécutions de programmes sans exécuter ces derniers.

Elle se distingue ainsi de l'analyse dynamique, ou test, qui revient à essayer le programme sur différentes entrées censément représentatives, afin de vérifier s'il produit toujours des résultats attendus sur ces entrées.

Méthodes formelles

L'analyse statique englobe une famille de méthodes formelles qui dérivent automatiquement de l'information sur le comportement de logiciels ou de matériels informatiques. Un application possible de l'analyse statique est l'aide automatisée au débogage, en particulier la recherche d'erreurs à l'exécution – gross modo, des évènements qui forcent le programme à « planter ».

L'analyse de programmes – y compris la recherche d'erreurs possibles à l'exécution – est indécidable : il n'existe aucune méthode « mécanique » qui peut toujours répondre sans se tromper au vu d'un programme si celui-ci peut ou non produire des erreurs à l'exécution. Ceci est un résultat mathématique fondé sur des résultats d'Alonzo Church, Kurt Gödel et Alan Turing dans les années 1930 (voir le problème de l'arrêt et le théorème de Rice).

Il existe deux grandes familles d'analyses statiques formelles de programmes:

• le model checking considère des systèmes à état fini, ou qui peuvent être réduits vers des systèmes à états finis par abstraction;
• l'analyse statique par interprétation abstraite approxime le comportement du système, soit par au dessus (considérant plus de comportements que

L'intérêt du monde industriel pour des outils d'analyse statique, spécialement pour le développement de logiciels critiques, s'est développé à la suite de l'explosion du vol inaugural de la fusée Ariane, laquelle a explosé à la suite d'un bogue informatique – sans doute une des bogues les plus chers de l'histoire.