Résumé/Abstract:
L'augmentation de la puissance du matériel informatique, d'une
facteur 106 pendant les 25 dernières années a
entraîné une explosion comparable de la taille des programmes. Le
champ d'application des très grands programmes (de 1 à 40
millions de lignes) va probablement s'élargir
considérablement au cours de la prochaine décade. Ces
très grands programmes devront être construits à des
coûts raisonnables et devront ensuite être maintenus et
modifiés tout au long de leur durée de vie (souvent plus de
20 ans). La taille et le rendement des équipes d'analyse, de
programmation et de maintenance de ces programmes ne peuvent pas croître
dans des proportions similaires. À un taux d'erreur fréquent (et
certainement un peu optimiste) d'une erreur par millier de lignes, de tels
programmes énormes risquent de devenir très rapidement
ingérables, en particulier pour les systèmes dont la
sûreté est critique. C'est pourquoi, à notre avis, le
\emph{problème de la sûreté du logiciel} sera
probablement un problème majeur pour les sociétés
modernes hautement informatisées.
Ces dernières années, de nombreux progrès ont
été réalisés sur les outils
méthodologiques (améliorant les capacités
intellectuelles humaines) pour concevoir des logiciels complexes et des
outils mécaniques (utilisant l'ordinateur) pour aider le
programmeur à raisonner sur des programmes.
Les outils mécaniques de vérification de programmes assistés par
ordinateur ont d'abord été conçus empiriquement en exécutant ou en
simulant le programmes dans un grand nombre d'environnements
suffisamment représentatifs des exécutions réellement possibles.
Cependant les techniques de test du code compilé sur des jeux de
données ou de simulation sur un modèle du programme source passent
difficilement à l'échelle et offrent souvent une faible couverture du
comportement dynamique du programme.
Les méthodes formelles de vérification tentent de prouver
mécaniquement que toutes les exécutions du programme sont correctes
dans tous les environnement spécifiés. Ces méthodes comprennent les
méthodes déductives, la vérification de modèle << model
checking >>, le typage et l'analyse statique de
programmes.
Comme la vérification formelle de programme est indécidable, donc non
complètement mécanisable, toutes ces méthodes sont partielles ou
incomplètes. Les problèmes d'indécidabilité et de très grande
complexité sont toujours résolus en utilisant une forme
d'approximation. Ceci signifie que les outils mécaniques
souffriront toujours de limitations pratiques en espace mémoire et en
temps de calcul. De ce fait ils devront toujours reposer sur des
hypothèses de finitude, utiliser des semi-algorithmes (ne se terminant
pas dans certains cas), requérir des interactions avec les
utilisateurs ou encore devront considérer seulement certaines formes
de programmes et/ou de spécifications. Les outils de vérification
mécanisée de programmes sont donc tous assez similaires et différent
essentiellement dans les choix des approximations qui sont faites pour
gérer ces problèmes d'indécidabilité ou de complexité.
L'objectif de l'interprétation abstraite est de formaliser cette
notion d'approximation dans un cadre mathématique unifié.
Nous illustrons informellement l'idée d'abstraction appliquée
à la sémantique des langages de programmation puis aux
différentes méthodes formelles, en insistant plus
particulièrement sur l'analyse statique. L'idée principale
est que pour raisonner ou calculer sur une système complexe, il est
nécessaire de perdre de l'information, de sorte que l'observation du
système doit être soit partielle soit à un haut niveau
d'abstraction.
Dans cette optique, nous comparons l'analyse statique avec les
méthodes déductives, le typage et la vérification de modèle. Les
fondements ainsi que les avantages et désavantages de ces quatre
outils sont rapidement passés en revue, y compris quand ils sont
combinés.
Nous suggérons une alternative combinant des méthodes formelles et
informelles. Cette méthode de vérification par test abstrait
est conceptuellement proche du test classique de programmes. Elle a
de bonnes chances d'être acceptée par les informaticiens
professionnels car elle ne remet pas considérablement en cause les
méthodes couramment utilisées dans l'industrie du logiciel.
\bibitem{Cousot00-ASPROM-Talk}
P{.} Cousot.
\newblock Interpr{\'e}tation Abstraite.
\newblock << Journées sur la Süreté des Logiciels >>
organisées par l'ASPROM et le CRITT-CCST, UIMM, 56, avenue
de Wagram, Paris 17e. 24 et 25 Octobre 2000.
@unpublished{Cousot00-ASPROM-Talk,
author = {Cousot, P{.}},
title = {Interpr{\'e}tation Abstraite},
note = {<< Journées sur la Süreté des Logiciels >>
organisées par l'ASPROM et le CRITT-CCST, UIMM, 56, avenue
de Wagram, Paris 17e},
month = {24 et 25 \oct},
year = 2000,
}