Jean-Raymond Abrial, Z, Socrate, B, Event-B, Rodin

 The presentation reviews CLEARSY’s two decades of experience applying formal methods, particularly the B method and Atelier B, across safety-critical domains. It highlights the successful industrial deployment of B in railway signaling and control systems, where formally specified and proved software has replaced extensive testing, and formal data validation could prevent accidents during exploitation such as overspeed incidents. The talk also presents the CLEARSY Safety Platform, a SIL4-certified safety computer that integrates redundant execution and formal programming, now deployed in railways and autonomous mobility projects. Beyond rail, formal methods have been applied in smart card certification and emerging autonomous mobility systems, with emphasis on standards, safety proofs, and lessons learned. The conclusion stresses that B remains a living, evolving technology, sustained by certified tools, industrial adoption, and growing requirements in tenders, demon...

  https://www.researchgate.net/publication/381519799_Proving_B_with_Atelier_B Abstract. The article focuses on the continuous improvement of Atelier B’s automatic proof capabilities since its industrialisation in the 90s.The evolution of Atelier B addressed challenges in proof obligations gen-eration and optimisation, adapting to new languages like Event-B andincorporating newer formats for easier analysis and third-party proverconnections. Significant developments include enhancing the proof system to handle complex proof obligations efficiently and integrating external provers for improved proof capabilities. The article also showcases B’s industrial applications in critical sectors, emphasising the method’s im-portance in safety-critical software development and the ongoing effortsto facilitate proof activities and integrate AI for better proof automation

 Mon Jean-Raymond Dominique Cansell (Lessy) dominique.cansell@gmail.com   Jean-Raymond n’est pas à moi. Il est à tout le monde. Si j’emploie ”mon” c’est parce que ce texte est aussi mon histoire, mon histoire autour des travaux communs avec ceux de Jean-Raymond. Je vous prie de m’excuser. Ce n’est pas un texte scientifique. Le lecteur pourra facilement trouver les papiers dont je parle dans ce document.      J’ai eu extrêmement de chance de le rencontrer et surtout de travailler avec lui. Je n’étais pas vraiment prédestiné à le rencontrer. À Metz je fais peu de recherche et j’enseigne l’algorithmique en utilisant la preuve très tôt avec une importance pour l’algorithmique récursive. Par contre, je ne le savais pas encore, j’avais le bagage mathématique pour faire les preuves en B.      En 1997 je décide de rejoindre l’équipe de Dominique Méry à Nancy. Je ne travaille pas directement sur B. Comme B n’était pas un langage récursif ...

  From Safe Rails To Autonomous Realms August 2025 DOI: 10.13140/RG.2.2.11454.96321 Conference: TAROS 2025 At: York, UK Affiliation: ClearSy System Engineering Lab: Thierry Lecomte's Lab  Thierry Lecomte presents CLEARSY’s journey from safety-critical railway automation to broader applications in autonomous mobility. Drawing from global deployments of automatic train systems, we show how railways function as large-scale robotic systems with embedded autonomy, localization, and fail-safe mechanisms. We then explore CLEARSY’s innovations in ground,aerial, and underwater autonomy, highlighting shared challenges in navigation, sensor fusion, and environment interaction. The role of advanced sensors, robust hardware, and formal modeling is emphasized across all domains. A core theme is the integration of safety, verification, and validation into robotics design—rooted in CLEARSY’s railway experience. The talk also addresses the transition from deterministic systems to co...

  Deux sens : Premier sens :  interprétation : attribution d'un sens à des énoncés formels de sorte qu'ils soient vérifiés La géométrie devient un modèle d'un langage formel, plutôt que la formalisation de propriétés idéalisées à partir d'observation de l'espace sensible. Étude des relations entre ensembles d'énoncés et ensembles de modèles de ces énoncés. Un modèle d'un énoncé fait dans un langage formel est une interprétation  (association d'un sens aux symboles du langage formel) où cet énoncé est vrai. Deuxième sens :  associer à une "réalité empirique" un énoncé formel. Minsky : Un objet O est un modèle d'une réalité R si O permet des répondre aux questions que l'on se pose sur R 

" Mathematics may be defined as the the subject in which we never know what we are talking about, not whether what we are saying is true "    Bertrand Russel In 'Recent Work on the Principles of Mathematics', International Monthly (1901) «  [...] les mathématiques sont la seule science où l'on sait  toujours de quoi l'on parle et où l'on est certain que ce que l'on  dit est vrai » * Emile Borel, après avoir cité B. Russell in Les grands courants  de la pensée mathématique, dir. par Le Lionnais F.    https://fr.wikipedia.org/wiki/%C3%89mile_Borel   https://en.wikipedia.org/wiki/%C3%89mile_Borel     *  « [...] mathematics is a science in which one never knows what you're talking about or if what you're saying is true" Bertrand Russell (1818) « [...] mathematics is the only science in which we know what we are talking about and where we are certain that what we are talking about says is true" Emile Borel, after quoting B...

 Nous recopions ici un tweet de  Etienne KLEIN @EtienneKlein · J’eus la chance, jeune, d’être étudiant d’été au @CERN  Un jour, le grand Victor Weisskopf, physicien splendide, commença son cours en nous expliquant qu’il avait passé sa vie à se demander si les objets mathématiques ont ou non une réalité physique : ne sont-ils qu’une invention humaine, un simple langage, ou ont-ils une existence indépendante de nous ? Il cita Platon, Aristote, Kant et Husserl, car bien sûr, le monsieur avait des lettres. Puis il entama son cours proprement dit. Pour les besoins d’une démonstration, il dut tracer à la craie un repère à trois dimensions. Suivant la règle, il représenta les axes Ox et Oy dans le plan même du tableau, puis figura l'axe Oz, perpendiculaire aux deux premiers, par un simple point entouré d'un cercle, donnant l'impression que cet axe jaillissait tel un bâton hors du tableau. Quelques minutes plus tard, alors qu’il s’apprêtait à passer devant la fi...