Posts

" People Disliked It " (extract from From Z to B and then Event-B: Assigning Proofs to Meaningful Programs)

Abrial, JR. (2013). From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_1   In this article you will find the history of B and line 14 of the Paris metro .  You will find the French version in the JRA conference at the Collège de France When writing the first paper on Z and starting to spread the idea of using a settheoretic notation to write a specification before writing a program, I received sometimes very negative answers. Some days at that time, I was invited to give a series of lectures at a Summer School but when the organizers saw the subject of my presentation, they canceled my visit, telling me that this subject was not relevant to computer scientists. I discovered then that set theory had a bad reputation among computer scientists in A...
Post a Comment
Read more

Je me souviens de l'INRETS

Je viens de recevoir un message me disant "Tu as le bonjour de Philippe Bon". Puis un autre me donnant l'adresse de courriel. Je ne savais pas que l'INRETS était maintenant dans une université. Et comme pour aller de Bordeaux à Clermont, pardon, à Lyon ! il faut passer par Paris, normal que cette université soit à Paris. Ben dame ! comme on dit à Nantes, Ben couillon ! comme on dit à Poitiers, Boudu con comme on dit à Toulouse. Evident ! on traite de transports !   Ah oui, bien sûr! l'INRETS  Pengfei Sun, Philippe Bon, Simon Collart-Dutilleul. A Joint Development of Coloured Petri Nets and the B Method in Critical Systems. Journal of Universal Computer Science, 2015, 21 (12), pp.1654- 1683.hal-01266935    https://fr.wikipedia.org/wiki/Institut_national_de_recherche_sur_les_transports_et_leur_s%C3%A9curit%C3%A9 "L’ Institut national de recherche sur les transports et leur sécurité ( INRETS ), créé par le décret n o  85-984 du 18 septembre 1985 [ 1 ] , était...
Post a Comment
Read more

Videotorium : Have we learned from the Wasa disaster? (J.-R. Abrial) , 19th September 2019, Grand Challenges of Informatics, Verified software

  https://kifu.videotorium.hu/en/recordings/1674/have-we-learned-from-the-wasa-disaster
Post a Comment
Read more

Atelier B, from Steria to Clearsy

Image
https://fr.wikipedia.org/wiki/Steria   De 1990 à 2000 1993 : Démarrage de l’industrialisation Atelier B pour une utilisation dans les logiciels de sécurité METEOR 1994 : Distribution de la première version Atelier B 1998 : Version industrielle de l’Atelier B et mise en service du métro METEOR De 2000 à 2010 2001 : Création de CLEARSY pour développer la méthode B. Deux agences : Aix-en-Provence et Paris. 2002 : Première version d’un langage formel système. Utilisation de la méthode B pour la réalisation des principes de fonctionnement des voitures Peugeot 206, 307, 407 (Documentation du fonctionnel). 2003 : Création de l’activité Sûreté de Fonctionnement (SDF) 2004 : Mise à disposition d’un outil gratuit d’utilisation de la méthode B pour les académiques : B4Free 2005 : Réalisation de spécification de systèmes industriels avec la méthode B. 2006 : Version Beta Test d’un outil de spécification formelle de système : Composys. – Mise en service du s...
Post a Comment
Read more

Spécifier ou comment matérialiser l'abstrait" (To specify, or how to materialize the abstract) (J.R. Abrial), The TSI article has been found!

  We searched for it for over a year, in France and elsewhere. Dominique Cansell has found the TSI issue number. We will tell you how to access it.   http://dominique.cansell.free.fr/JRA-TSI-1984.pdf   "Spécifier ou comment matérialiser l'abstrait" Jean-Raymond Abrial, 1984 TSI 0752-4072/84/03/201-19 AFCET-Bordas Illustration with an example. For people interested into the genesis of B  
Post a Comment
Read more

" Ne vouloir être ni conseillé ni corrigé sur son ouvrage est un pédantisme " (La Bruyère)/"To refuse to be advised or corrected on one's work is pedantry" (La Bruyère)

Image
 cité par Hubert Haddad in Le nouveau magasin d'écriture,  Editions Z, Zulma Vous êtes bien sur un blog consacré entre autres à Z ! Je vous conseille ce livre, 939 pages. A éviter au lit, il est trop lourd.     Quoted by Hubert Haddad in *Le nouveau magasin d'écriture*, Editions Z, Zulma You're definitely on a blog dedicated, among other things, to Z! I recommend this book, 939 pages. Avoid reading it in bed; it's too heavy.     Alors n'hésitez pas à critiquer, corriger les billets de ce blog. So feel free to criticize and correct the posts on this blog.  
Post a Comment
Read more

B#

 Abrial, JR. (2003). B # : Toward a Synthesis between Z and B. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_12 In this paper, I present some ideas and principles underlying the realization of a new project called B # . This project follows the main ideas and principles already at work in B, but it also follows a number of older concepts developed in Z. In B # , the intent is to have a formal system to be used to model complex system in general, not only software systems.  https://link.springer.com/chapter/10.1007/3-540-44880-2_12  
Post a Comment
Read more