Ce séminaire, intitulé « Logiciel prouvé avec B pour des automatismes sécuritaires à bas coût et à haut niveau d’intégrité », est axé sur les dernières innovations concernant le développement d’applications critiques avec la méthode formelle B:
« L’Atelier B a été utilisé de manière intensive pour le développement d’applications critiques, principalement dans le domaine ferroviaire. Le pilote automatique du métro METEOR de la ligne 14 parisienne, prouvé avec B et sans aucun bug détecté depuis sa mise en service en 1998, est le meilleur exemple d’application de cette technologie utilisée aujourd’hui dans plus de 25% des métros automatiques dans le monde. Au fil du temps, de nouvelles techniques de modélisation et leurs outils associés sont apparus, avec pour objectif la réduction du temps de développement et de validation par preuve. Le raffinement automatique, la preuve intégrée à l’édition de modèle ainsi que l’édition de modèle abstrait sont de nouvelles fonctionnalités testées et en cours de déploiement sur des systèmes critiques. Plus récemment, une nouvelle architecture sécurisée a émergé, basée sur deux processeurs et combinant du logiciel (méthode B) et des techniques matérielles compatibles avec les normes EN5012{6, 8, 9}. Cette plateforme d’exécution a été utilisée pour plusieurs applications ferroviaires certifiées (métro de São Paulo, métro de Stockholm). Elle a été choisie pour être financée dans le cadre d’un projet de R&D collaboratif français (LCHIP) afin d’obtenir un produit générique capable de faciliter le développement d’applications SIL4. La génération de code et la validation par preuve vont être complétement automatisées. L’IDE associé va accepter n’importe quel langage métier (DSL) au travers d’une API publique. Au cours du séminaire, des techniques modernes de développement avec B et la plateforme d’exécution sécurisée à bas coût vont être présentées en détail. «