Expert systèmes critiques

CBTC RATP Ligne 14 (Siemens)



Validation des règles ajoutées en langage formel B



L'atelier B est un outil de de développement et de preuve formelle de logiciels
Il a été utilisé pour la première fois par Siemens dans le cadre du projet de métro en automatisme intégral Météor, pour la ligne 14 du métro Parisien.
Les programmes développés en B sont prouvés par l'atelier. Cette preuve est automatique autant que faire se peut, appuyée par une aide manuelle. La preuve se fonde sur des règles mathématiques, pour la plupart codée dans l'atelier et pour certaine ajoutées manuellement.
Ma mission consistait à démontrer la validité des règles ajoutées manuellement. Il s'agissait de démonstrations mathématiques de théorèmes, une fois les règles traduites en théorèmes : hypothèses et assertions.
J'ai donné le meilleur de ma formation de mathématicienne pour cette tâche.