Applications des techniques formelles au logiciel (Arago 20)

Les méthodes dans le cycle de vie. Pourquoi des méthodes formelles ? Éléments de classification des méthodes formelles. Les expériences industrielles. Application de la méthode B dans l'industrie ferroviaire. Spécifications formelles à Aerospatiale. SAO+/Lustre : utilisation d'une technique formelle en environnement ferroviaire non critique. LDS appliqué à la modélisation et à la validation des processus communicants. Plan de défense - Formalisation du cahier des charges du point central à l'aide de spécifications algébriques. Techniques formelles pour le développement d'une passerelle de sécurité au niveau ITSEC-E41. Vérification formelle de protocoles de commerce électronique : une expérience. Utilisation et développement des méthodes formelles à l'étranger. Les expériences et recherches prometteuses. Évaluation des méthodes formelles chez Dassault aviation. Application des méthodes formelles au développement des logiciels automobiles embarqués. Utilisation d'un environnement de logique temporelle pour la validation et le test d'un système de commandes électriques d'avion. Approche pour la validation et la vérification formelles de systèmes d'interaction homme-machine. Méthodes formelles pour la vérification de logiciels critiques. Descartes et l'enjeu de la programmation automatique. L'architecture informatique du lanceur Ariane 5.

L'objectif est d'analyser l'intérêt que présente l'application des techniques formelles au développement et à la maintenance des systèmes informatiques. L'ouvrage montre comment les principales limitations aux conditions d'utilisation de ces techniques 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.