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

  https://www.academia.edu/13917699/On_Teaching_the_Concept_of_Refinement_with_B?email_work_card=abstract-read-more   Joanna Tomasik Guy Vidal-Naquet Computer Science Department SUPELEC Gif-sur-Yvette, France     Abstract The concept of refinement is central to the development of software. It appears in various forms in the different methodologies taught to students. A key point in the B method is the validation of the refinement step. The B methodology exhibits mathematical properties of correct refinements, and also automatically checkable conditions that ensure those properties. Some of the main pedagogical difficulties that the present authors found in teaching B centered around the notions linked to refinement, at the conceptual level, and at the tool level. Many papers have been published on the general benefits of the B method. This paper will focus on the specific concepts linked to refinements, and on the ones which need special care. We argue that, althoug...

  Jean-Raymond Abrial    Jean-Claude Boussard Jean-Claude Boussard (1938 – 2021) Jean-Claude Boussard, ingénieur de l’Institut de Radioélectricité de Grenoble (IRG) et licencié ès-sciences a soutenu en juin 1964 une thèse de doctorat ès-Sciences Appliquées : “Étude et réalisation d’un compilateur ALGOL60 pour ordinateur 7040/44”. La réalisation de compilateurs a été une activité intense de ce qu’on appelait à l’époque le Laboratoire de Calcul et qui deviendra l’IMAG. Pas moins de 19 compilateurs ont été produits à Grenoble pour différents langages (COBOL en 1963 par Jean-Loup Baer, puis ALGOL60 essentiellement par la suite), toutes ces activités ayant été supervisées dès 1961 par Louis Bolliet recruté comme ingénieur CNRS en 1956. Le jury de la thèse de Jean-Claude Boussard comprenait Jean Kuntzmann (1912-1992) professeur de mathématiques appliquées et fondateur du Laboratoire de Calcul, Noël Gastinel (1925-1984) p...

    ⚡ The B WORKBOOK is now available on CLEARSY 's GitHub: ( https://lnkd.in/dZCJJzah ). After several months of collaborative effort, this first version (122 pages) can now be used as a resource for training in formal methods and for teaching the B method. We warmly thank the contributors and reviewers from Europe and South America who made this release possible. ✅ The B WORKBOOK currently offers 7 exercises of increasing complexity, providing a step-by-step introduction to Atelier B. It covers the main phases of development: formal specification, implementation, proof, code generation, and compilation of the final executable. Each exercise comes with: * modelling files * proof files with automatic demonstrations * complementary manual source code and Makefile for Unix environments (Windows WSL, Linux, MacOS) * instructions for animating models with ProB. 🔎 A next iteration (planned for 2026) will extend the scope with new exercises on: * Event-B modelling * graphica...

Christian Julnet qui en 1970-71 a eu Jean-Raymond Abrial comme professeur à Grenoble m'a écrit que Jean-Raymond venait à la faculté avec une Peugeot comme celle de Colombo.   https://commons.wikimedia.org/wiki/File:Peter_Falk_Colombo_1973.jpg Comme Bernard Suffrin (1) fut à Grenoble avec Jean-Raymond (mais pas à la même époque), je lui ai demandé s'il avait voyagé avec cette Peugeot. https://commons.wikimedia.org/wiki/File:Lieutenant_Colombo%27s_Peugeot_403_Cabriolet_at_Universal_Studios,_Los_Angeles_(16526700486).jpg   Sa réponse : "I never saw the Peugeot, but he would have loved “Colombo”. We talked of Peter Falk (the actor who played Colombo) a few times. Falk was a strong and generous ally in the anti-Vietnam-war movement while I was in the US. J-R had studied at Stanford (Master’s) before his navy conscription, and had witnessed the very beginning of the movement. "    https://fr.wikipedia.org/wiki/Columbo "La particularité la plus marquante de la série...

 " Nous connaissons au moins un jeu où tout le monde gagne, et où, à gagner, tout le monde, enrichi, enrichit l'enjeu. L'échange ou la communication scientifique, fondement de la rationalité du savoir rigoureux, exact, efficace, est,en précision, ce jeu-là. " Michel Serres, , Hermes III, La traduction, Éditions de Minuit, 1974  https://fr.wikipedia.org/wiki/Michel_Serres   https://www.researchgate.net/publication/394026329_Event-B_et_la_plateforme_Rodin     "We know at least one game where everyone wins, and where, by winning, everyone enriches themselves, enriching the stakes. Scientific exchange or communication, the foundation of the rationality of rigorous, exact, effective knowledge, is, precisely, that game."   https://en.wikipedia.org/wiki/Michel_Serres  

  https://www.clearsy.com/ https://www.clearsy.com/en/   https://www.clearsy.com/en/tools/       https://www.systerel.fr/ https://blog.systerel.fr/fr/   https://www.systerel.fr/en/     https://fr.wikipedia.org/wiki/Aix-en-Provence   https://en.wikipedia.org/wiki/Aix-en-Provence  

  https://blog.systerel.fr/fr/posts/2021-06/b-method-for-dynamic-structures-in-s2opc/ The software B method has so far been mainly used in the industrial world to develop safety critical software with very basic memory management limited to arrays of fixed size defined at compilation time. We present here an alternative approach for modelling software based on a more classic memory management with dynamically allocated complex data structures accessed through pointers Note This article is almost taken as is from our publication : “Modelling dynamic data structures with the b method” published in International Conference on Abstract State Machines, Alloy, B, TLA , VDM , and Z, 420–424. Springer, 2018 .    

         Photo transmise par D.C. "tous droits de traduction, de reproduction et d'adaptation réservés pour tous les pays, y compris l'URSS et les pays scandinaves" (les grands-parents comprendront !) Jean-Raymond Abrial nous a préparé à cela dans les pages 115 à 120 du B-Book. Mais vous n'y trouverez pas les petits-enfants que les Anglais nomment les grands-enfants !   Nous vous laissons compléter le B-Book.  Photo provided by D.C. "All translation, reproduction, and adaptation rights reserved for all countries, including the USSR and Scandinavian countries" (grandparents will understand!) Jean-Raymond Abrial has prepared us for this on pages 115 to 120 of the B-Book. But you won't find the grandchildren that the English call grandchildren! We'll leave it up to you to complete the B-Book. 

    https://www.academia.edu/70751897/Bunch_theory_applications_axioms_and_models Abstract In his book A practical theory of programming [7], Eric Hehner proposes and applies a remarkably radical reformulation of set theory, in which the collection and packaging of elements are seen as sepa- rate activities. This provides for unpackaged collections, referred to as “bunches”. Bunches allow us to reason about non-determinism at the level of terms, and, very remarkably, allow us to reason about the conceptual entity “nothing”, which is just an empty bunch (and very different from an empty set). This eliminates mathematical “gaps” caused by undefined terms. We compare the use of bunches with other approaches to this problem, and we illustrate the use of Bunch Theory in formulating program semantic combining non-deterministic, preferential, and probabilistic choice. We show how an existing ax- iomatisation of set theory can be extended to incorporate bunches, and we provide and val...

  https://velo.wiki.ls2n.fr/doku.php?id=velo:js2025   replay visio zoom partie 1 replay visio partie 2 A replay visio partie 2 B replay visio zoom partie 3 replay visio zoom partie 4  

 “Z caused a good deal of confusion on the pronunciation stakes. The English and even Scots and some French call it Zed. The Americans call it Zee and get confused when we correct them Zed. But Ib had his own distinctive pronunciation: Zet. ” ( Bill Roscoe , In Memoriam Ib Sorensen)   https://dictionary.cambridge.org/pronunciation/english/z   https://dictionary.cambridge.org/pronunciation/english/b?q=B   En français B se prononce [be] 

1 Introduction A l'Arsenal d'Indret sur la rive droite de la Loire, le SBBD Socrate et le langage LTR étaient utilisés. Mais nous n'avons pu retrouver le personnel qui collaborait à l'enseignant du département informatique de l'IUT de Nantes et qui les utilisait. Il existe peu de documentation disponible actuellement sur le langage LTR. Nous commençons à présenter ce que nous avons trouvé sur la Toile. Puis nous reproduisons ce qu'a bien voulu nous adresser pour reproduction David Andreu qui fut enseignant-chercheur à l'Université Montpellier II avant de créer une entreprise. On y lira comment il a utilisé LTR pour son enseignement, son cours, des exemples de travaux pratiques et d'examens. Enfin nous fournissons les informations reçues la semaine précédant la journée scientifique de Nantes sur le langage LTR, J.-R Abrial et le Centre de Programmation de la Marine.   La suite ici : https://velo.wiki.ls2n.fr/doku.php?id=velo:js2025    

The 12th instalment of the ABZ conference will be held in Tokyo, Japan, co-located with FM 2026 (The 27th International Symposium on Formal Methods) .   https://conf.researchr.org/home/fm-2026 abz2026@nii.ac.jp  

7th International Conference on "Putting into Practice Methods and Tools for Information System Design", proceedings, October, 10-12, 1995, Nantes (France) in co-operation with ZUG and BUG  

http://www.iste.co.uk/index.php?f=a&ACTION=View&id=100       Contents Part 1: State-Based Approaches 1. Z , J. Bowen. 2. SAZ , F. Polack. 3. B , H. Diab and M. Frappier. 4. From UML Diagrams to B Specifications, R. Laleau and A. Mammar. 5. UML+Z: Augmenting UML with Z, N. Amalio, F. Polack and S. Stepney. 6. ASM, E. Börger, A. Gargantini and E. Riccobene. 7. TLA+, L. Lamport. Part 2: Event-Based Approaches 8. Action Systems, J. Sinclair. 9. Event B , D.Cansell and D. Méry. 10. VHDL, L. Pierre. 11. Estelle, E. Lallet and J.-L. Raffy. 12. SDL, P. Poizat. 13. (E)-Lotos, K. Turner and M. Sighireanu. 14. EB3, F. Gervais and M. Frappier. Part 3: Other Formal Approaches 15. Casl, H. Baumeister and D. Bert. 16. Coq, J.-F. Monin. 17. Petri Nets, A. Choquet-Geniet and P. Richard. 18. Petri Nets with Objects, C. Sibertin-Blanc. Part 4: Comparison and Glossary 19. A Comparison of the Specification Methods, M. Frappier, H. Habrias and P. Poizat. 20. Glossary, H. Habrias, ...

  https://www.research-collection.ethz.ch/server/api/core/bitstreams/e4877fdb-b00b-4722-9012-f6a8e3e00901/content ETH Library Event-B patterns and their tool support Report Author(s): Hoang, Thai Son; Fürst, Andreas; Abrial, Jean-Raymond Publication date: 2012 Permanent link: https://doi.org/https://doi.org/10.3929/ethz-a-007224905 Rights / license: In Copyright - Non-Commercial Use Permitted  Summary: Event-B has given developers the opportunity to construct models of complex systems that are correct-by-construction. However, there is no systematic approach, especially in terms of reuse, which could help with the construction of these models. We introduce the notion of design patterns within the framework of Event-B to shorten this gap. Our approach preserves the correctness of the models, which is critical in formal methods and also reduces the proving effort. Within our approach, an Event-B design pattern is just another model devoted to the formalisation of a typi...

  https://link.springer.com/content/pdf/10.1007/978-3-642-30885-7_13.pdf Formalizing Hybrid Systems with Event-B Jean-Raymond Abrial1, Wen Su2, and Huibiao Zhu2 1 Marseille, France jrabrial@neuf.fr 2 Software Engineering Institute, East China Normal University {wensu,hbzhu}@sei.ecnu.edu.cn Abstract. This paper1 contains the development of hybrid systems in Event-B and the Rodin Platform2 . It follows the seminal approach in- troduced at the turn of the century in Action Systems. Many examples illustrate our approach 

 

  http://www.grupo-aes.com.br/site/home/?id=95 Welcome to BDD'08, the First Brazilian Workshop on B Method Dissemination.   This Event will be presented twice in 2008 as following: In Salvador - Bahia - Brazil, August, 26th as a Satellite event of  SBMF 2008  (  subscription at SBMF2008 site )   In São Paulo - SP - Brazil, August, 28th as a special event of IPT (Instituto de Pesquisas Tecnológicas do Estado de São Paulo) - Register here     Comments, suggestions and doubts, send an e-mail to: agrj@aes.com.br  

  https://teachingbconference.blogspot.com/2018/01/verification-corner-modeling-refinement.html https://www.youtube.com/watch?v=fSWZWXx5ixc In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.

  https://teachingbconference.blogspot.com/2018/01/lectures-of-jean-raymond-abrial-on-b.html Lecture 1  https://www.youtube.com/watch?v=2GP1pJINVT4 Lecture 2 https://www.youtube.com/watch?v=M8nvVaZ74wA Lecture 3 https://www.youtube.com/watch?v=Y5OUtq8cdV8  Mini-course around Event-B and Rodin Developping sequential programs https://www.youtube.com/watch?v=C0tpgPOKAyg This lecture gives a status report of the hypervisor we are developing using Event-B. https://www.youtube.com/watch?v=i-GKHZAWWjU

  https://hal.science/hal-04993432v1/file/final_proceedings_tfmb2010.pdf Journées scientifiques - Université de Nantes (FR) - 2010 From Research to Teaching Formal Methods: The B Method TFM-B’201O imprim´e par IUT de Nantes (Université de Nantes), rue M. Joffre, 44000 Nantes Publié par APCB ISBN 978-2-9512461-1-9 EAN 9782951246119 Tirage achevé en juin 2010 - Prix : 10 e Dépôt légal : juin 2010 

 Nous avons un draft (avec très peu de corrections typographiques faites de la main de J.-R.)  de cet article que nous avait adressé Jean-Raymond Abrial. Les idées développées dans cet article qui n'a semble-t-il jamais été publié (merci à ceux qui en connaîtraient une publication de m'en informer) sont exposées dans les pages 12-14 de Modeling in Event-B, Cambridge, 2010 Voici : https://saintyrieixlaperche.wordpress.com/2025/09/12/le-cahier-des-charges-contenu-forme-et-analyse-en-vue-de-la-formalisation-par-j-r-abrial-consultant/   We have a draft (with very few typographical corrections made by J.-R.) of this article, which Jean-Raymond Abrial sent us. The ideas developed in this article, which apparently has never been published (please let me know if anyone knows of a publication), are presented on pages 12-14 of Modeling in Event-B, Cambridge, 2010.   Here : https://saintyrieixlaperche.wordpress.com/2025/09/12/le-cahier-des-charges-contenu-forme-et-analyse...

Hybrid event: *BCS-FACS AGM & Peter Landin Semantics Seminar* *Formal Methods: Whence and Whither* BCS London office (near Moorgate underground station) and on Zoom, 4 December 2025 Speaker: *J < https://sites.google.com/site/jpbowen/ >*Jonathan Bowen < https://sites.google.com/site/jpbowen/ >* (Chair of FACS)Agenda   " 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 viabl...

 Merci à Jean-Pierre Giraudin qui nous a donné l'ensemble des documents sur l'étude de cas avec mise en œuvre du SGBD Socrate. Extraits         On trouvera l'explication de la notation dans  Les 16 cas de relations binaires avec les papygrammes, NIAM, Merise, UML, Z0, B, notation de E. Codd (schémas relationnels n-aires) et la notation Oc https://jean-raymond-abrial.blogspot.com/2025/09/les-16-cas-de-relations-binaires-avec.html  

  Les 16 cas de relations binaires avec les papygrammes, NIAM, Merise, UML, Z0, B, notation de E. Codd (schémas relationnels n-aires) et la notation Oc Habrias Henri Henri.Habrias@univ-nantes.fr   1 Notation Z0, B, etc . — La notation créée par J.R. Abrial a évoluée au cours du temps. Il y eu les premiers écrits d’Abrial sur Z , puis après son séjour à Oxford , la notation décrite par J.M. Spivey dans La Notation Z (traduction française de Michel Lemoine, Masson). En ce qui concerne la notation des relations, celle de B est la même que celle de Spivey pour les 16 cas que nous présentons. En pratique en B on donne la spécification d’une relation dans le sens le plus contraint. Par exemple, on préférera une fonction totale à la relation inverse qui serait une relation "quelconque". — Avec la notation NIAM, il n’y a que deux symboles, celui d’unicité (représenté par une ligne, comme dans la notation du modèle relationnel n-aire on souligne la clé de la relation-type) et celui...

Claude Boksenbaum organized the Second B Conference at the Corum in Montpellier in April 1998 . He also designed the t-shirt bearing the words "Let it B"   B'98: Recent Advances in the Development and Use of the B Method Second International B Conference, Montpellier, France, April 22-24, 1998, Proceedings It was an opportunity for me to return to the city where I began studying computer science at the IUT (University Institute of Technology) on rue du Cardinal de Cabrières. Pézenas is known, among other things, for two figures: Molière and Boby Lapointe. Boby Lapointe is known among computer scientists for having invented the Bibi-binary. https://en.wikipedia.org/wiki/Bibi-binary#References https://en.wikipedia.org/wiki/Boby_Lapointe "He is best known for his songs peppered with puns, spoonerisms, alliterations, and paronomasia, sometimes to the point of deceiving ears." "After obtaining his baccalaureate, he began preparing at the Montpellier high school[...

 C'est  Claude Boksenbaum  qui a organisé en avril 1998 la deuxième conférence B au Corum à Montpellier. Et qui a conçu le tee-shirt portant l'inscription Let it B B'98: Recent Advances in the Development and Use of the B Method Second International B Conference, Montpellier, France, April 22-24, 1998, Proceeding   Ce fut pour moi l'occasion de revenir dans la ville où j'ai commencé l'informatique à l'IUT rue du Cardinal de Cabrières. Pézenas est une ville connue entre autres, par deux personnages, Molière et Boby Lapointe. Boby Lapointe est connu des informaticiens pour avoir inventé le Bibi-binaire.   https://en.wikipedia.org/wiki/Bibi-binary#References   https://fr.wikipedia.org/wiki/Boby_Lapointe   "Il est surtout connu pour ses chansons parsemées de calembours , de contrepèteries , d' allitérations et de paronomases , au point parfois de constituer des trompe-oreilles . "  "Après avoir obte...

  https://www.jaist.ac.jp/~bjorner/ae-is-budapest/talks/Sept19am3_Abrial.pdf Have we Learned from the Vasa Disaster? Jean-Raymond Abrial ETH Zurich September 19th 2006 

  https://www.academia.edu/52001742/Refinement_decomposition_and_instantiation_of_discrete_models_Application_to_Event_B?email_work_card=view-paper&li=0 https://doi.org/10.5555/1365972.1365974   Original PDF Related Refinement, Decomposition and Instantiation of Discrete Models Jean-Raymond Abrial ETHZ Zurich, Switzerland jabrial@inf.ethz.ch It is my belief that the people in charge of the development of large and complex computer systems must adopt a point of view shared by all mature engineering disciplines, namely that of using an artifact to reason about their future system during its construction. In these disciplines, people use blue-prints (in the wider sense of the term) which allows them to reason formally during the very construction process. Most of the time, in our discipline, we do not use such artifacts. This results in a very heavy testing phase on the final product, which is well known to happen quite often too late. Th...