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

  "If fire is regarded as a thing - for the pre-Socratics it is one of the 4 elements - and not as a reaction between several things, we cannot understand anything. Now observation presents fire to us as a thing." The vision of fire as an entity, an object with its properties blocked scientific invention. It was in 1785 that Lavoisier destroyed the substantial conception of fire and the phlogiston theory, by carrying out the analysis and synthesis of water. "Jouary J.P. 2002 Enseigner le vérité ? Essai sur les sciences et leurs représentations. L ’Harmattan

” Si le feu est regardé comme une chose - pour les présocratiques il est un des 4 éléments -, et non comme une réaction entre plusieurs choses, on ne peut rien comprendre. Or l’observation nous présente le feu comme une chose ”. La vision du feu comme une entité, un objet avec ses propriétés a bloqué l’invention scientifique. C’est en 1785 que Lavoisier a détruit la conception substantielle du feu et la théorie phlogistique, en réalisant l ’analyse et la synthèse de l ’eau. " Jouary J.P. 2002 Enseigner le vérité ? Essai sur les sciences et leurs représentations. L ’Harmattan    

 Voici quelques extraits des archives de l'association APCB, Association de Pilotage des Conférences internationales B. On y verra le passage des conférences B aux conférences BZ. Maintenant nous avons ABZ. Here are some excerpts from the archives of the APCB association, Association de Pilotage des Conférences internationales B. We will see the transition from the B conferences to the BZ conferences. Now we have ABZ. La déclaration de l'association au Journal Officiel de la République Française  Dépôt légal d'actes de conférences Vers la première conférence BZ  Une des compositions de APCB  

  https://www.nosta.gov.cn/pc/en/awards/awardees2/1511.shtml " The awarding ceremony of the 2016 National Science and Technology International Cooperation Award was held on January 9th, 2017 at the Great Hall of the People in Beijing. The adjunct professor of the School of Computer Science and Software Engineering at East China Normal University, a famous French computer scientist, Jean-Raymond Abria won the International Science and Technology Cooperation Award of the People's Republic of China. East China Normal University is the only institution in Shanghai with the award. "   See the photographs in the article cited. https://en.wikipedia.org/wiki/Great_Hall_of_the_People    

  https://www.youtube.com/watch?v=J3mYPI2_d84 Michael Leuschel • 1er Professor of Computer Science 1 j      For fun I encoded the barber paradox in Event-B: ``` context BarberParadox sets People constants barber shaves axioms @axm1 barber∈People @axm2 shaves ∈ People ↔ People @axm3 ∀x· x∈People ⇒ (x↦x ∉ shaves ⇔ barber↦x ∈ shaves) theorem @thm1 barber↦barber ∈ shaves theorem @thm2 barber↦barber ∉ shaves theorem @thm3 1=2 end ``` and the answer of the Rodin auto-provers is, yes, the barber shaves himself and he also does not shave himself and 1=2. The answer of ProB is that the axioms are in...

They have said, we are going to remove unit tests and remove integration tests,  which is very interesting because the tests for such embedded systems  It's extremely expensive. They removed from the after because the before  was and in October 98, the launch of line 14. Since then, no problem.  Initially, Matra Transports was absolutely against the use of B.  Mr. Hennebert was absolutely incredible. He said, "You're against, okay,  so you're going to do both, one with your techniques and also the  technique with B and then we'll see." They opened the taps of course and little by little little ones ended up  being convinced and in particular the engineers did very well adapted  to this new technology because it was necessary to prove And in particular  some of these proofs are automatic but others are interactive, i.e. the user  has to use the tool to help the computer to prove. [...] For line 1, what  is remarkable is that for...

During the 80s, I had contacts with the RATP, which planned a semi-automatic  metro on the RER line A and which had developed a very important embedded system.  But at the last minute, the managers had to make the final decision.  I was contacted by Claude Hennebert, RATP engineer who is an extremely  interesting individual because he was at the RATP and he was neither an ENA  nor a polytechnician, he was blocked. It was someone who was high enough  in the hierarchy so close enough to the taps but at the same time who had kept  a very good technical mind, so he contacted me and he told me "We would like  to do a technical audit". Lasted three weeks. I met some very interesting  people and had to answer questions.  Are the means used to ensure that the product does it correspond to its  initial specification? So I do my study and then at a big meeting, there were people from the RATP  and also the manufacturers who manufactured ...

 Ce courriel de Christophe Prazuck nous en appris plus sur LTR, langage sur lequel Jean-Raymond Abrial a travaillé au CPM à Paris.   Monsieur, pour répondre à vos interrogations, j'ai interrogé l'amiral Edouard Guillaud, ancien chef d'état-major des armées et acteur passionné du Centre de Programmation de la Marine (CPM)  Il écrit  " Il y a eu au moins deux versions de LTR utilisées (LTR1 qui était une transcription de la version US, puis LTR 2, française et plus puissante) et une en gestation (LTR3) à l'époque de la mise au point d'ADA. Le CPM s'intéressait aussi à l'époque à des langages récents tels que C, C+ et C++, en raisons des bouleversements apportés par les puces modernes.  Je pense que le réponses seraient complètes si elles étaient posées à un ingénieur de l'armement  en poste au CPM de la grande époque.  En particulier à l'Ingénieur en Chef de l'Armement (ICA) Pascal Grojean, remarquable spécialiste visionna...

  https://blog.systerel.fr/fr/posts/2024-11/un-nouveau-coeur-pour-ovado/ Depuis plus de 10 ans le département MOP réalise des prestations de validation de données avec l’outil OVADO²® propriété de la RATP , qui est maintenu et distribué par Systerel. L’outil OVADO²® est principalement utilisé pour vérifier de manière automatisée des règles sur des données de paramétrage de systèmes ferroviaires. Après avoir réalisé un modèle des données et des règles à vérifier dans un langage formel (le langage B OVADO ), on utilise l’outil sur un jeu de données à vérifier. Classiquement l’outil sert à vérifier que : les données du système respectent certaines règles de niveau système, les données des équipements ont été calculées correctement à partir des données système, les données des équipements respectent certaines contraintes de niveau équipement.   https://blog.systerel.fr/fr/posts/2023-01/generating-and-verifying-configuration-data-with-ovado/ ...

  https://blog.systerel.fr/fr/posts/2025-12/fuite-memoire-preuveB/ "La fuite mémoire désigne une situation dans laquelle des emplacements de mémoire vive, alloués d’une manière dynamique, ne sont jamais libérés pendant ou à la fin d’une exécution d’une application. En conséquence, ces emplacements mémoire ne sont plus accessibles d’une manière correcte et au fur et à mesure, la mémoire sera saturée. La saturation de la mémoire peut causer l’arrêt de l’exécution des applications ou forcer le redémarrage de l’ordinateur." 

FACS FACTS Issue 2026-1 January 2026 Tributes to Jean-Raymond Abrial https://www.bcs.org/media/veppnllv/facs-jan26.pdf Tributes to Jean-Raymond Abrial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 by Jonathan P. Bowen and Henri Habrias Testimonies from Bernard Amy, researcher and mountaineer, and Jean-Louis and Odette Bernezat, mountain and Saharan guides . . . . . . . . . . . . . . . . . . . . ...............19 by Bernard Amy Jean-Raymond Abrial: A Rich Friendship . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 by Egon Börger Jean-Raymond Abrial, an appreciation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 by Michael Butler Mine Jean-Raymond . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .  30 by Dominique Cansell What I owe to Jean-Raymond Abrial . . . ...

  https://www.bcs.org/events-calendar/2025/december/hybrid-facs-agm-and-peter-landin-semantics-seminar Title: Formal Methods: Whence and Whither Abstract: Alan Turing arguably wrote the first paper on formal methods over 75 years ago.Since then, there have been claims and counterclaims about formal methods. Tool development has been slow but aided by Moore’s Law with the increasing power of computers. Although formal methods are not widespread in practical usage at a heavyweight level, their influence has crept into software engineering practice to the extent that they are no longer necessarily called formal methods in their use. In addition, in areas where safety and security are important, with the increasing use of computers in such applications, formal methods are a viable way to improve the reliability of such software-based systems. Their use in hardware, where a mistake can be very costly, is also important. This talk explores the journey of form...

  https://jean-raymond-abrial.blogspot.com/2025/09/le-diner-de-gala-de-la-deuxieme.html https://jean-raymond-abrial.blogspot.com/2025/09/gala-dinner-for-second-international-b.html