Produire des systèmes informatiques répondant à des exigences de qualité données, à des coûts et dans des délais raisonnables est non seulement l'un des grands enjeux économiques de notre temps, mais aussi un défi scientifique et technologique important. Il l'est d'autant plus actuellement que l'utilisation massive des technologies informatiques renforce les exigences de fiabilité dans un nombre croissant de domaines d'application, tels que les transports terrestres, l'avionique, l'énergie nucléaire, les systèmes de commande temps réel, ainsi que les réseaux de communications ou les applications bancaires

L'approche par les méthodes formelles (spécification, validation et synthèse) est la méthode proposée en informatique depuis de longues années, mais celle-ci est restée cantonnée au niveau de la recherche universitaire et n'a pas encore vraiment percé au niveau industriel.

Ce livre, rapport de synthèse du Groupe de travail "Méthodes formelles en logiciel" de l'Observatoire Francais des Techniques Avancées (OFTA), montre comment les principales limitations aux conditions d'utilisation des techniques formelles (temps de calcul et place mémoire importants, ésotérisme et manque de lisibilité des formalismes, diffusion insuffisante des outils et des connaissances...) sont en train d'être levées et que la résolution des problèmes de productivité et de fiabilité du logiciel va pouvoir progresser de manière significative.

Coordinateur : Michel GONDRAN (EDF, Direction des Etudes et Recherches), assisté de Henri HABRIAS (Université de Nantes, Institut de Recherche en Informatique de Nantes (IRIN))

Autres membres : Patrick BEHM (Matra Transport International) - Patrick BLANLUET (Sagem S.A.) - Dominique BOLIGNANO (Bull S.A.) - Olivier BRIHAYE (CSEE Transport) - Christine CHOPPY (Université de Nantes, IRIN) - Philippe CONTENSOU (Aerospatiale Aéronautique) - Catherine DELLIAUX (Gaz de France) - Pierre DESFORGES (RATP) - Gilles DOWEK (INRIA) - Georges GALLAIS (Sagem S.A.) - Gérard HUET (INRIA) - René JACQUART (ONERA-CERT) - Francis KLAY (CNET, France Telecom) - Amaury LEGAIT (Syseca) - Simon MARICHALAR (Renault) - Fernando MEJIA (GEC Alsthom Transport) - Pierre MICHEL (ONERA-CERT) - Jean-François MONIN (CNET, France Telecom) ; François PILARSKI (Aerospatiale Aéronautique) - Laurent PONTHIEU (EDF) - Jacques PRINTZ (CNAM) - Jacques RAGUIDEAU (LETI, CEA) - Philippe SARAZIN (DGA, DSP) - Gérard SERMONDADAZ (Gaz de France) - Joseph SIFAKIS (CNRS-Verimag)

Conclusions et recommandations du Groupe

Argumentaire

Les méthodes dans le cycle de vie

I. Pourquoi des méthodes formelles ? - II. Eléments de classification des méthodes formelles

Les expériences industrielles

III. Application de la méthode B dans l'industrie ferroviaire - IV. Spécifications formelles à Aerospatiale - V. SAO+/Lustre : utilisation d'une technique formelle en environnement ferroviaire non critique - VI. LDS appliqué à la modélisation et à la validation des processus communicants - VII. Plan de Défense - Formalisation du cahier des charges du Point Central à l'aide de spécifications algébriques - VIII. Techniques formelles pour le développement d'une passerelle de sécurité au niveau ITSEC-E41 - IX. Vérification formelle de protocoles de commerce électronique : une expérience - X. Utilisation et développement des méthodes formelles à l'étranger

Les expériences et recherches prometteuses

XI. Evaluation des méthodes formelles chez Dassault Aviation - XII. Application des méthodes formelles au développement des logiciels automobiles embarqués - XIII. Utilisation d'un environnement de logique temporelle pour la validation et le test d'un système de commandes électriques d'avion - XIV. Approche pour la validation et la vérification formelles de systèmes d'Interaction homme-machine - XV. Méthodes formelles pour la vérification de logiciels critiques - XVI. Descartes et l'enjeu de la programmation automatique - XVII. L'architecture informatique du lanceur Ariane 5

Annexes techniques

I. La méthode B - II. Aperçu du langage Lustre - III. La vérification formelle de circuits VLSI en milieu industriel - IV. Evaluation des systèmes critiques : critères ITSEC et méthodes formelles - V. Comment obtenir les informations sur les méthodes et les produits ?

__________________________________________________________________________ARAGO 20 (286 pages) peut être acheté directement à l'OFTA au prix de 600 F TTC. La commande doit être accompagnée du paiement en cas d'achat à titre personnel ou d'un bon de commande établi par l'organisme prenant l'achat à sa charge.