Vérification d'un logiciel temps-réel distribué : étude comparative des environnements B, SDT et Spin

International audienceDans le cadre du développement d'une application industrielle liée au do- maine médical, entrepris à l'ENSIETA de Brest, un groupe de travail s'est formé en collaboration avec des membres de l'IRCyN de Nantes et de l'ENST Bretagne. Cette application de nature distribuée et ayant un caractère cri- tique mettant en jeu des vies humaines est un bon support pour évaluer l'utilisation de méthodes formelles en portant l'accent sur les aspects de fiabilité et de sécurité. Ce groupe s'intéresse donc à des outils qui facilitent l'écriture de spécifcations formelles et qui permettent d'effectuer des verifications. Les outils étudiés au sein du groupe sont : Spin, outil d'origine universitaire Hol91], l'Atelier B Abr96], et l'environnement TAU/SDT de Telelogic Tel98]. L'intérêt scientifique de ce travail en cours est d'utiliser conjointement ces outils sur une même application, de les comparer et de tenter de déga- ger par la suite une méthodologie appréhendable par des ingénieurs dans le monde industriel dans le cadre d'applications embarquées. L'objectif visé est de disposer d'un ensemble d'outils complémentaires, utilisable par des développeurs confrontés à des contraintes de gestion de projets et qui puisse être une aide à la conception de logiciels temps réel et distribués