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

  Bertrand Meyer With Claude Baudoin : Méthodes de Programmation   (Programming Methodology), Eyrolles, Paris, 1978 ; third revised edition,  661 pages, 1984. Translation: Russian (Mir Publishing) " We wrote this book fresh out of school and managed to convince the publisher to include everything (other publishers wanted us to trim it down to 250 pages). It is a compendium of programming methodology, programming techniques, fundamental algorithms and data structures. It emphasizes program correctness, through assertion techniques, and software architecture. The chapter on programming methodology contains the first ever published description of the Z specification language anywhere (as far as I know), in a very early form. The book was extremely successful in France, both as a textbook and for engineers in industry; incredibly, it still seems to be in print. The Russian translation was also widely circulated and I still meet people from Russia who tell me this...

  Une ascension de Jean-Raymond Abrial, parmi de nombreuses autres.     https://publications.americanalpineclub.org/articles/12197205100   Publication Year: 1972. A Game of Patience The Northeast Summit of the Rooster Comb BERNARD AMY, Club Alpin Français Translated by H. Adams Carter   Summary of Statistics: AREA: Alaska Range, just south of Mount McKinley. ASCENT : Rooster Comb’s northeast summit, 9680 feet, (not the highest point), August 3, 1971 (Abrial, Amy, Bleuer, Coqueugniot, Cordier, Ruph). PERSONNEL: Jean-Raymond Abrial, Bernard Amy, Herbert Bleuer, Joël Coqueugniot, Patrick Cordier, Francois Ruph, Mademoiselle Marie-Francoise Gay.  voir : https://jean-raymond-abrial.blogspot.com/2025/07/temoignages-de-bernard-amy-chercheur-et.html    

  🤝 As part of a project funded by the French National Research Agency ( ANR (Agence nationale de la recherche) ), CLEARSY is collaborating with Loria (Nancy), CRIL (Lens) and the Université de Liège to improve the mathematical demonstration tools of Atelier B. 🧮 When Atelier B is used to develop secure software, it produces mathematical proof obligations that must then be resolved. ⚙️ Atelier B's demonstration tools (provers) already enable a large proportion of these to be resolved automatically. 🚀 The project “Enhancing B Language Reasoners with SAT and SMT Techniques” aims to improve the efficiency of these demonstrators. ✅ The initial results are already conclusive! 📊 On a test bench of 681,285 proof obligations, techniques based on SAT-type consistency verification tools and SMT-type consistency checking tools have enabled us to increase the number of automatically proven proof obligations from 74% to 87%. 🎯 TARGET: Over 90% by the end of the project in March ...

. Ce jeudi 5 juin 2025 ont eu lieu à Marseille les obsèques de Jean Raymond Abrial, un des plus éminents et des plus originaux créateurs français en sciences de l’information (Jean-Raymond Abrial — Wikipédia). Du monde de la recherche internationale émergent des hommages soulignant tel ou tel souvenir, trait de sa personnalité de chercheur ou de sa recherche, de son œuvre, mais qui mieux que lui-même n’a décrit, dans une conférence au Collège de France de 2015, ce que fut son projet de recherche et ses réalisations? https://lnkd.in/dzNE4Rir Quel fut le moteur de ce parcours intellectuel d’une quarantaine d’années? L’accumulation de richesses matérielles? certainement pas, c’était un ascète. Le pouvoir au sein des hiérarchies politiques, économiques, sociales et académiques? Il s’en tint à l’écart. Alors peut-être, selon l'expression de Carl Gustav Jacobi, reprise dans le titre d’un livre du mathématicien Jean Dieudonné, “l’honneur de l’esprit humain”. ...

 amine AIT AMEUR IRIT/INPT-ENSEEIHT Toulouse, France yamine@enseeiht.fr Idir AIT SADOUNE LRI/CentraleSupelec Gif Sur Yvette, France idir.aitsadoune@centralesupelec.fr Kahina HACID IRIT/INPT-ENSEEIHT Toulouse, France kahina.hacid@enseeiht.fr Linda MOHAND OUSSAID LRI/CentraleSupelec Gif Sur Yvette, France linda.mohandoussaid@centralesupelec.fr This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms,theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories. https://arxiv.org/pdf/1805.05518

Publication type Book Chapter DOI 10.1007/978-3-319-66854-3_12 Journal 2017 , Lecture Notes in Computer Science Model and Data Engineering , p. 153-166 Publisher Springer International Publishing Authors Linda Mohand-Oussaid, Idir Ait-Sadoune  

  Jean-Louis Boulanger Book Editor(s): Jean-Louis Boulanger First published: 26 June 2014 https://doi.org/10.1002/9781119002727.ch6   https://onlinelibrary.wiley.com/doi/10.1002/9781119002727.ch6   S ummary This chapter shows how it is possible to combine the advantages of the B method in order to design a secure digital circuit that may be easily developed and does not need a design test. The goal is to make use of the B method to produce the electronic or numeric circuits. The B method due to J.R Abrial is a formal method for the incremental development of specifications and their refinements down to an implementation. VHDL is one of the most important tools for describing the electronic circuits. It depends on the conception of modules. The most recent imperative languages like VHDL include facilities as manipulations of a vector without explicit length or functions...

  Jean-Raymond Abrial , Dominique Cansell https://lib.jucs.org/article/28407/   Journal of Universal Computer Science, vol. 11, no. 5 (2005), 744-770 submitted: 30/11/04, accepted: 31/1/05, appeared: 28/5/05 Abstract This paper contains a completely formal (and mechanically proved) development of some algorithms dealing with a linked list supposed to be shared by various processes. These algorithms are executed in a highly concurrent fashion by an unknown number of such independent processes. These algorithms have been first presented in [MS96] by M.M. Michael and M.L. Scott. Two other developments of the same algorithms have been proposed recently in [YS03] (using the 3VMC Model Checker developed by E. Yahav) and in [DGLM04] (using I/O Automata and PVS). Keywords atomicity, concurrency, refinement, formal proof, prover  

 Dominique Cansell, Dominique Méry 2003    Computing and Informatics, Vol. 22, 2003, 1–31   Abstract. B is a method for specifying, designing and coding software systems. It is based on Zermelo-Fraenkel set theory with the axiom of choice, the concept of generalized substitution and on structuring mechanisms (machine,refinement, implementation). The concept of refinement is the key notion for developing B models of (software) systems in an incremental way. B models are accompanied by mathematical proofs that justify them. Proofs of B models convince the user (designer or specifier) that the (software) system is effectively correct. We provide a survey of the underlying logic of the B method and the semantic concepts related to the B method; we detail the B development process partially supported by the mechanical engine of the prover. Keywords: Events, Actions, Systems, Refinement, Proof, Validation, Formal Method. https://www.imm.dtu.dk/~dibj/cai/cai-b.pdf ...

  https://www.lacl.fr/valarcher/Publi/ABZ2010.pdf B-ASM: Specification of ASM `a la B David Michel1?, Frédéric Gervais2, Pierre Valarcher2 1 LIX, CNRS, Polytechnique School, 91128 Palaiseau, France dmichel@lix.polytechnique.fr 2 LACL, Université Paris-Est IUT Sénart Fontainebleau, Dpt. informatique, 77300 Fontainebleau, France {frederic.gervais,pierre.valarcher}@univ-paris-est.fr Abstract. We try to recover the proof correctness strength of the B method and the simplicity of the Abstract State Machine model (ASM ) by constructing a B-ASM language. The language inherits from the lan- guage of substitution and from ASM program. The process of refinement leads us to a program expressed in the ASM syntax only. As each step of refinement is correct towards the specification, we obtain an ASM that is proved to be correct towards the specificatio 

  https://archiv.infsec.ethz.ch/intranet_secured/education/as09/evtB/course_material_secured/ieee-handout.pdf/ieee-handout.pdf  

https://www.scitepress.org/PublishedPapers/2005/25715/      L. Yeung W. and R. P. H. Leung K. (2005). Deriving Test Cases from B Machines Using Class Vectors . In Proceedings of the 3rd International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems - Volume 1: MSVVEIS, (ICEIS 2005) ISBN 972-8865-22-8, pages 71-76. DOI: 10.5220/0002571500710076   Abstract This paper proposes a specification-based testing method for use in conjunction with the B method. The method aims to derive a set of legitimate class vectors from a B machine specification and it takes into account the structure and semantics of the latter. A procedure for test case generation is given. One advantage of the method is its potential to be integrated with the B method via its support tools.  

M. Carnot ; C. DaSilva ; B. Dehbonei ; F. Mejia   https://ieeexplore.ieee.org/document/285893 Abstract: A description is given of the process of software development for critical systems using the B-Methodology designed by J.R. Abrial. The author explains the insights of the B formal development process: specification and implementation through refinements where each refinement step is proved using axioms based on the first-order predicate logic and an extension of the Zermelo set theory. They present the techniques and related tools that facilitate the process of realizing and proving programs. Three tools are described: the typechecker, the proof-obligation generator and the prover. Two industrial critical software systems have been carried out using this methodology: the subway speed control under final on-site tests ( approximately 3000 lines of Modula-2) and the KVS French train speed control that is in the integration test phase ( approximately 15000 lines of A...

  http://www.artist-embedded.org/docs/Events/2010/UML_FM/SLIDES/Keynote_Abrial_Slides.pdf   l

  https://pure.ul.ie/en/publications/ten-commandments-ten-years-on-lessons-for-asm-b-z-and-vsr-net Ten commandments ten years on: Lessons for ASM, B, Z and VSR-net   Just over a decade ago, a paper Ten Commandments of Formal Methods [16] suggested some guidelines to help ensure the success of a formal methods project. It proposed ten important requirements (or "commandments") for formal developers to consider and follow, based on our knowledge of several industrial application success stories, most of which have been reported in more detail in two books [32,33]. The paper was surprisingly popular, is still widely referenced, and used as required reading in a number of formal methods courses. However, not all have agreed with some of our commandments, feeling that they may not be valid in the long-term. We re-examine the original commandments over ten years on, and consider their validity in the light of a further decade of industrial best practice and experiences, ...

  https://czt.sourceforge.net/z2b/index.html C Z T : Community Z Tools Tools for developing and reasoning about Z specifications CZT / Z to B / Introduction Translator from Z to B This project provides a translator from Z specifications to B abstract machines. The B notation was designed by J.R. Abrial, who was also one of the designers of Z notation. Their mathematical toolkits are very similar, but B has more support for modularity and refinement (including an executable sublanguage). The standard reference for B method is “The B-Book: Assigning Programs to Meanings” , by J-R. Abrial, Cambridge University Press, 1996, ISBN 0 521 49619 5. This translator converts a Z specification (which currently must contain just one section) into the ASCII ( *.mch ) syntax used by the B tools (Atelier B and the B toolkit). The goal of the translator is to give Z users access to the ref...

  https://lib.jucs.org/article/28407/ Abstract This paper contains a completely formal (and mechanically proved) development of some algorithms dealing with a linked list supposed to be shared by various processes. These algorithms are executed in a highly concurrent fashion by an unknown number of such independent processes. These algorithms have been first presented in [MS96] by M.M. Michael and M.L. Scott. Two other developments of the same algorithms have been proposed recently in [YS03] (using the 3VMC Model Checker developed by E. Yahav) and in [DGLM04] (using I/O Automata and PVS). Keywords atomicity, concurrency, refinement, formal proof, prover

  https://archiv.infsec.ethz.ch/intranet_secured/education/as09/evtB/course_material_secured/evtb-slides.pdf/evtb-slides.pdf  

  https://www.microsoft.com/en-us/research/video/mini-course-around-event-b-and-rodin-hypervisor/   July 1, 2011 Jean-Raymond Abrial and Rustan Leino | MSR  

    Integrated Formal Methods: 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings Pages 18 - 35 https://doi.org/10.1007/978-3-031-07727-2_2 Authors : Yamine Aït-Ameur , Guillaume Dupont , Ismail Mendil , Dominique Méry , Marc Pantel , Peter Rivière , Neeraj K. Singh  Authors Info & Claims     Event-B offers a rigorous state-based framework for designing critical systems. Models describe state changes (transitions), and invariant preservation is ensured by inductive proofs over execution traces. In a correct model, such changes transform safe states into safe states, effectively defining a partial function, whose domain prevents ill-defined state changes. Moreover, a state can be formalised as a complex data type, and as such it is accompanied by operators whose correct use is ensured by well-definedness (WD) conditions (partial functions). This paper proposes to define transitions explicitly as partial...

  https://eprints.soton.ac.uk/250549/ Book Review The B-Book: Assigning Programs to Meanings by J.-R. Abrial Cambridge University Press 1996. ISBN 0-521-49619-5. 779pp. Hardbound. Appears in The Computer Journal , Vol.40.1 (1997):59-61, ISSN 0010-4620. B is a formal method in the same vein as Z and VDM. Such methods are often referred to as 'model oriented' since they describe system behaviour using an explicit model of the system state along with operations on the state. The B method was developed mostly by Jean-Raymond Abrial and was influenced by his work on the development of Z. Apart from some notational differences, what distinguishes B from Z is that B aims to cover a broader range of the development cycle from specification to coding, whereas Z is perhaps more suited to earlier stages of the development cycle. To quote from the introduction, 'B is a method for specifying, designing and coding software systems'. The method makes use of formal refine...

  https://link.springer.com/article/10.1007/s10270-010-0183-7 "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 typical sub-problem. As a result, we can use patterns to construct a model which can subsequently be used as a pattern to construct a larger model. We also present the interaction between developers and the tool support within the associated RODIN Platform of Event-B. The approach has been applied successfully to some medium-size industrial cas...

  Jean-Raymond Abrial (consultant): ” Le zéro défaut n’existe pas mais on peut tout de même s’en approcher “ Publié le 11 janvier 2002 à 00:00    https://www.01net.com/actualites/jean-raymond-abrial-consultant-le-zero-defaut-nexiste-pas-mais-on-peut-tout-de-meme-sen-approcher-173964.html   Les méthodes formelles sont en mesure de garantir des logiciels plus fiables. Pourtant, elles ont encore du mal à percer. Le contexte De nos jours, il est devenu courant, de parler de qualité logicielle, en entreprise. Paradoxalement, l’utilisation des méthodes formelles, qui garantissent une plus grande fiabilité des programmes, a du mal à se généraliser. Jean-Raymond Abrial, l’inventeur de la méthode B, donne son point de vue sur la situation. Bien que permettant d’accroître la fiabilité des logiciels, les méthodes formelles sont encore peu utilisée...

  http://dominique.cansell.free.fr/ I officially stopped my research more than 15 years ago but I worked sometime with Jean-Raymond Abrial when he was stuck in a proof or a development. In 2017 JRA asked me to work on the Goodstein sequence (ordinals) In 2019 we worked on a Protocop inspired by the Lamport's Paxos one. This work will be presented in ABZ2025 the original paper Rodin archive for the direct approach Rodin archive for the constructive approach JRA's Profile using PP and SMT End of 2020 JRA asked me to work on his new instantiation (component). I think it's a good thing and I've use it to develop many context and theorems. This work was done in the EBRP ANR project my EBRP activity I am retired in march 2025 and my unique objective is to propagate JRA's ideas.