Les erreurs dans les logiciels qu'il est bien difficile d'éviter ont des conséquences imprévisibles et parfois financièrement voire humainement catastrophiques. Le rôle grandissant des logiciels informatiques va conduire le grand public à prendre conscience des effets néfastes des erreurs logicielles. Par conséquent la société sera plus exigeante quant à la responsabilité grandissante des informaticiens dans ce domaine, qu'elle soit collective ou individuelle. Comment échapper à l'échec ? Très certainement en améliorant la qualité des méthodes de production de logiciels et en multipliant les précautions lors du processus de validation et de vérification de la fiabilité des logiciels.

        L'objet de ce séminaire est de présenter les techniques d'analyse statique de logiciels par interprétation abstraite et de montrer comment elles peuvent être utilisées pour la vérification formelle en complément des méthodes classiques de test, de simulation ou de validation de code ou de systèmes informatiques.

        Après une introduction générale sur les méthodes employées, la journée comprend des exposés sur l'analyse statique de logiciels critiques, de systèmes temporisés et de code parallèle, distribué ou mobile et les exploitations de l'analyse statique dans un contexte industriel.

8H45	ACCUEIL
9h00	INTERPRÉTATION ABSTRAITE : FONDEMENTS ET APPLICATIONS par Patrick COUSOT, professeur, laboratoire d'informatique, École normale supérieure, Paris.         Un analyseur statique est un outil entièrement automatisé permettant de prédire les comportements à l'exécution d'un programme par le seul examen de son texte. Il est utilisé pour répondre automatiquement à des questions sur les comportements possibles des programmes à l'exécution. Pour ce faire, l'idée de base qui nous a guidé pour concevoir l'interprétation abstraite est qu'il suffit de considérer une approximation pertinente de la sémantique des programmes. Cette sémantique décrit formellement tous les comportements possibles d'un programme. C'est un modèle mathématique qui représente les structures créées par le programme ainsi que leur évolution au cours de toutes les exécutions possibles du programme. Des théorèmes généraux d'indécidabilité montrent qu'il n'est pas possible de calculer automatiquement et de manière exacte la sémantique d'un programme. L'interprétation abstraite permet de résoudre ce problème en se restreignant à des sous-ensembles pertinents des informations observées sur les comportements des programmes.          Dans une première partie, on expliquera les principes de l'interprétation abstraite c'est-à-dire de la théorie permettant de construire des analyseurs statiques cohérents et fiables à partir de la sémantique d'un programme et d'une spécification des propriétés observables des comportements du programme. Elle a de nombreux champs d'application comme la conception de sémantiques, le typage, le model-checking abstrait et l'analyse statique qui fait l'objet de ce séminaire.          Dans une deuxième partie, nous abordons deux applications à l'analyse statique. La première concerne la recherche d'erreurs à l'exécution. Il s'agit de déterminer quelles sont les erreurs comme le défaut d'initialisation, les dépassements de capacité (par exemple le dépassement des bornes de tableaux), les défauts de synchronisation, les pointeurs pendants, etc. qui sont certaines, potentielles ou impossibles à l'exécution.         La deuxième application concerne le test abstrait. Il s'agit de déterminer des conditions nécessaires pour qu'une spécification donnée par le programmeur soit satisfaite, ce qui permet de rechercher les erreurs.
10h30	PAUSE
10h45	VÉRIFICATION STATIQUE DE LOGICIELS CRITIQUES par Alain DEUTSCH, chargé de recherche, INRIA, Rocquencourt.
12h00	DÉJEUNER AVEC LES CONFÉRENCIERS
13h30	L'INTERPRÉTATION ABSTRAITE AU CEA par Éric GOUBAULT, CEA/Saclay, LETI/DEIN/SLA, 91191 Gif-sur-Yvette.         Le CEA a la charge « de donner la maîtrise de l'atome et de ses applications dans les domaines de la recherche, de l'énergie, de l'industrie, de la santé et de la défense ». Cela implique la maîtrise d'úuvre et l'intégration de métiers très variés, dont celui qui consiste à écrire des logiciels critiques ou de simulation (des réacteurs, mais aussi des armes) et à les valider (par exemple l'IPSN vérifie les programmes de contrôle/commande des réacteurs nucléaires). Depuis, les compétences développées commencent à s'exporter vers le domaine des logiciels "moins critiques".          C'est dans ce cadre que s'inscrira mon exposé, qui tentera d'expliquer en quoi l'analyse statique de code par interprétation abstraite répond aux besoins de validation des programmes qui nous sont confiés. Je traiterai donc principalement, de l'aide à la preuve et à la maintenance de code écrit en C, de la génération automatique de jeux de tests, du débogage "abstrait" de codes numériques et enfin de validation du comportement (correction des accès à des ressources partagées, absence de point mort, étude sous panne) de systèmes parallèles et distribués. Quelques exemples d'applications étudiées et de prototypes d'outils de vérification automatique seront donnés au cours de l'exposé.
14h45	ANALYSE STATIQUE POUR LA SÉCURITÉ DU CODE MOBILE par Arnaud VENET, laboratoire d'informatique, École normale supérieure, Paris.       Avec le développement des réseaux et de l'Internet, l'usage de code mobile téléchargeable va être certainement amené à se répandre dans l'industrie du logiciel. Or la conception de code mobile soulève de nouveaux problèmes de sécurité. En effet, un composant logiciel téléchargé ne doit pas compromettre l'intégrité et le bon fonctionnement du système dans lequel il s'insère. Nous ne parlons pas ici d'applets Java au comportement bridé mais de véritables agents mobiles pouvant accéder à toutes les ressources de la machine hôte (par exemple un composant offrant un nouveau service que l'on insère dans le système d'exploitation de son téléphone portable). La mise au point et la vérification de telles entités logicielles est très complexe car on ne sait pas à priori dans quel contexte elles vont évoluer. Il faudrait en théorie explorer toutes les interactions possibles du composant avec son environnement, ce qui est rarement faisable en pratique même pour du code de taille modeste.        Nous montrerons dans cet exposé comment l'analyse sémantique peut aider le concepteur de composants logiciels mobiles en lui procurant des outils entièrement automatisés permettant un examen exhaustif du code. Nous présenterons un prototype d'analyseur automatique qui est particulièrement bien adapté au domaine de la téléphonie.
16h00	PAUSE
16h15	VÉRIFICATION DE SYSTÈMES TEMPORISÉS À L'AIDE D'UNE ANALYSE DE RELATIONS LINÉAIRES par Nicolas HALBWACHS, directeur de recherche au CNRS, laboratoire VÉRIMAG, Grenoble.       L'analyse de relations linéaires est une interprétation abstraite dédiée à la synthèse automatique de relations linéaires vérifiées de manière invariante par les variables numériques d'un programme. Ce type d'analyse permet, par exemple, de découvrir qu'en un certain point de contrôle du programme, les relations x = 2y + z et x < 1 sont toujours satisfaites par les variables x, y et z.        Nous utilisons cette analyse en vérification de programmes, dans les nombreux cas où la vérification se ramène à montrer que certains point de contrôle ne sont pas accessibles : si les relations synthétisées ne sont pas satisfiables, le point de contrôle considéré ne peut pas être atteint.        Nous appliquons cette technique à la vérification de propriétés de deux types de modèles de systèmes temps réel : les programmes synchrones et les systèmes hybrides linéaires. Dans ces modèles, le temps est appréhendé au moyen de variables (compteurs, horloges) dont le comportement régulier est particulièrement bien capté par l'analyse. D'autre part, les systèmes temps réel sont ceux dont les erreurs peuvent avoir les conséquences les plus graves, et donc où la vérification formelle est un objectif particulièrement crucial.
17H30	DISCUSSION GÉNÉRALE avec les conférenciers.
18H00	FIN DU SÉMINAIRE.

à imprimer :