Ariane, Airbus et Agendas :
3 applications en logiciel de base

Amphi Gay-Lussac, 10h30,
18 mai 2005

Jean-Jacques Lévy (École polytechnique et Inria Rocquencourt)
En juin 1996, le vol 501 d'Ariane 5 s'est terminé au bout de 39 secondes à la suite d'un dépassement de capacité lors d'une conversion d'un nombre flottant en entier court sur 16 bits (en exécutant une partie inutile du programme de vol!). Une équipe de l'Inria a analysé le code du vol 502, en recherchant notamment l'utilisation des variables partagées entre processus concurrents. Cela a permis la découverte (avant exécution) de plusieurs erreurs de programmation. Une entreprise (Polyspace tech.) a été créée par Daniel Pilaud et Alain Deutsch à la suite de ce travail. Nous décrirons succinctement le genre d'approche utilisée.

Laurent Mauborgne (École polytechnique et École Normale Supérieure)
Astree est un système d'analyse statique de programmes temps-réels et embarqués. Il a été utilisé pour les programmes utilisés pour les commandes de vol électriques des Airbus A340 et A380. Astree fonctionne sur des programmes de 400000 lignes de C; il permet de garantir avec une très bonne précision l'absence d'erreurs tels que les divisions par zéro, les dépassements de capacité, les accès incorrects aux tableaux, les déréférencements de pointeurs nuls. L'analyseur s'appuie sur la théorie de l'interprétation abstraite développée par Patrick et Radhia Cousot. La base des techniques utilisées sera exposée brièvement.

Alan Schmitt (Inria Rhône-Alpes)
Face au nombre croissant de machines sur lesquelles nous stockons des données, tels des ordinateurs (fixes ou portables), des assistants personnels ou des téléphones, la question de la synchronisation de ces données prend de plus en plus d'importance. Nous présenterons tout d'abord Unison, un outil de synchronisation de fichiers multi-plateformes (Unix et Windows) développé par l'équipe de Benjamin Pierce à l'université de Pennsylvanie. Cet outil a une spécification formelle simple, que nous décrirons, qui le rend sûr et prévisible. Nous présenterons ensuite Harmony, une extension de Unison permettant de construire des outils de synchronisation pour le contenu de fichiers, tels des agendas, des calendriers ou des signets (bookmarks).