Posts

On Teaching the Concept of Refinement with B

  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...
Post a Comment
Read more

IFIP Working Conference On Data Base Management, Cargèse, Corsica, France, 1-5 April 1974

Image
  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...
Post a Comment
Read more

The B WORKBOOK

Image
    ⚡ 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...
Post a Comment
Read more

Colombo et la Peugeot403 Cabriolet

Image
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...
Post a Comment
Read more

un jeu où tout le monde gagne / one game where everyone wins (Michel Serres)

 " 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  
Post a Comment
Read more

Clearsy et Systerel

  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  
Post a Comment
Read more

Use of B method for dynamic structures in S2OPC, Frédéric Badeau Vincent Lacroix Vincent Monfort Laurent Voisin

  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 .    
Post a Comment
Read more