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

” 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 ...