Retour à la page d'accueil de l'action TOLÈRE
26-28 janvier 2000, Grenoble.
L'atelier, organisé par le groupe ADER (Aide au Développement Raisonné de Spécifications et de Programmes) et le Laboratoire Systèmes Réseaux de l'IMAG, s'est présenté comme un atelier qui favorise l'échange des idées entre la communauté universitaire et la communauté industrielle. La preuve est le fait que les trois tables rondes ont eu des invités du milieu industriel (Dassault Aviation, Trusted Logic, Alcatel, Gemplus, Vérilog, RATP et Schneider Electric) et que parmi les trois conférences invités, deux ont été aussi du milieu industriel.
Les thèmes principaux ont été :Parmi les conférences invités, Emmanuel Ledinot de Dassault Aviation a rapporté son expérience dans l'utilisation d'Esterel pour la spécification des tâches, dont le succès est déjà connu. De l'autre côté, l'essai d'appliquer Coq est pour le moment infructueux pour des problèmes de dimension industrielle pour lesquelles l'outil ne peut fournir des solutions en temps raisonnable.
Dominique Borrione de l'Université Joseph Fourier, Grenoble, a parlé de l'utilisation des méthodes formelles pour la vérification des systèmes intégrés digitaux. Sa conclusion est intéressante : elle parle de l'émergence d'un nouveau métier en micro-électronique, l'ingénieur de vérification. Son travail est la validation des nouveaux processeurs, des nouveaux systèmes embarquées ou bien des nouveaux algorithmes matériaux. Ses outils de travail sont les méthodes formelles et les logiciels basés sur ces méthodes.
La troisième conférence invitée, par Dominique Bogliano de Trusted Logic, était centrée sur l'application des méthodes formelles dans le domaine de la sécurité des systèmes informatiques. Il a montré l'émergence de besoins de sécurité dans les domaines civils, grâce au développement de l'internet, des réseaux d'entreprises et du commerce électronique. Cette émergence s'est effectuée à la suite d'une periode pendant laquelle les méthodes formelles étaient utilisés principalement dans un cadre militaire.
Les deux tables rondes, une sur UML et l'autre sur le problème de la validation (du système, du logiciel) ont eu comme but de familiariser les auditeurs du milieu universitaire avec, d'une part l'expérience des acteurs industriels dans l'utilisation des méthodes formelles, et d'autre part les prévisions sur l'avenir des méthodes formelles dans l'industrie. On a souligné le succès du model-checking ainsi que l'inadéquation des méthodes formelles comme Coq et PVS pour modéliser des problèmes de dimension industrielle. On a aussi montré que l'utilisation des méthodes formelles permettent de prendre en compte les besoins des tolérance aux pannes au moment où on démarre la spécification du système.
Les actes de la conférence contiennent les résumés des trois lectures invitées et des quinze articles présentés. Ils sont accessibles par internet sur le site web du LSR. Les articles sont divisés en deux groupes. 8 sont dédiés à une étude de cas proposée par les organisateurs : un système de contrôle d'accès à un ensemble de bâtiments. Les 7 autres couvrent un large spectre des méthodes formelles : B, Coq, PVS, UML, Pi-calcul, spécification algébrique et model-checking. A retenir l'approche de Mountassir, Bellegardde, Julliand et Masson du Laboratoire d'Informatique de l'Université de Besançon, qui présentent une coopération entre model-checking et preuve pour LTL qui peut fournir, dans les cas étudiés, des résultats meilleurs que l'application des algorithmes de model-checking pur.