Livres , vidéos, MOOC sur B et event-B


Henri Habrias
henri.habrias@univ-nantes.fr

1 Livres sur B

 
1.1 En anglais


 The B-Book, Assigning Programs to Meanings , Jean-Raymond Abrial,
Cambridge University Press , 1996, ISBN : 0-521-49619-5


 The B langage and Method, A Guide to Practical Formal Development,
Facit, Springer, 1996, ISBN : 3-540-76033-4


 Specication in B, An introduction using the B toolkit, Kevin Lano,
Howard Haughton, Imperial College Press, 1996, ISBN :1-86094-018-8


 Software Engineering with B, J.D. Wordsworth, AddisonWesley, 1996,
ISBN : 0-201-40356-0

the B-method  an introduction, Steve Schneider, Palgrave, 2001

 

Figure 1  Livres B en anglais
1
1.2 En français

 
 Spécication formelle avec B, Henri Habrias avec la collaboration de Didier
Bert, Jean-Yves Lafaye, Marie-Laure Potet, Hermes Sciences, Lavoisier,
ISBN : 2-7462-0302-2


 La Méthode B, concepts, démarche. Exemples d'applications, Karl Emeriau,
IUT de Nantes, Département informatique, 1997, ISBN :2-906082-
26-0


 Méthode B, sous la direction de Didier Bert, Henri Habrias, Véronique
Viguié Donzeau-Gouge, TSI, Volume 22, n°1, Hermes Lavoisier, 2003 ,
ISBN :2-7462-0651-X


Figure 2  Livres B en français


1.3 En chinois

 
Méthode B, Date de publication : 2004-1,par J-R Abrial ; Traduit par Qiu
Zongyan, Maison d'édition de l'industrie électronique, ISBN : 9787505393394
ISBN : 7505393391
Figure 3  Livres B en chinois
2


2 Livres sur Event-B 
 

2.1 En anglais

 
 Modeling in Event-B, System and Software Engineering, Jean-Raymond
Abrial, Cambridge University Press, 2010, ISBN : 978-0-521-89556-9


 Ken Robinson, System Modelling& Design Using Event-B, ©July 2007
Last updated : July 31, 2012 https://cgi.cse.unsw.edu.au/~cs2111/
PDF/SMD-KAR.pdf, Livre non publié


Figure 4  Event-B en anglais


2.2 En chinois


Figure 5  Event-B en chinois
Modeling in Event-B, System and
Software Engineering, Jean-Raymond
Abrial, Cambridge University Press
Traduit par Qiu Zongyan, Presse populaire
des postes et télécommuniucations,
septembre 2019


3 Documents sur Rodin


Abrial, Jean-Raymond and Metayer,
Christophe and Voisin, Laurent
(2009) Rodin Manual and Language
Denition. Manual. RODIN Project.
(Unpublished), last modied :19 Apr
2010 , 

Quatre documents PDF : User
Manual, Mathematical Language (outdated), Event-B notation, Mathematical
Language V2
https://web-archive.southampton.ac.uk/deploy-eprints.ecs.soton.
ac.uk/11/index.html
3


4 Vidéos

 
4.1 Cours de J.R. Abrial, 1994

 
Cet ensemble de cassettes vidéo n'a pas été transcrit sur un support moderne.
Dépôt à la BNF. Introduction à la méthode, 6 cassettes Description
matérielle : 1 cass. vidéo : coul., SECAM; 1/2 pouce VHS Description : Note :
Cours en direct de l'IUFM Nantes, centre Schmitt Copyright : Abrial, Jean-
Raymond, cop. 1994 Édition : Nantes : Institut universitaire de technologie
(Nantes) [éd.] ; Toulouse : Teknea [distrib.] , 1995 (DL) Producteur de vidéogrammes
: Jean-Raymond Abrial Distributeur : Teknea Éditeur commercial :
Institut universitaire de technologie. Nantes
Logique et preuve,méthode B Description matérielle : 1 brochure (26-49-26
p.) - 3 cass. vidéo (59 min, 46 min, 18 min) : ill., couv. ill. en coul. ; 30 cm ; coul.,
SECAM; 1/2 pouce VHS Description : Note : Cop. 1997 Édition : Marseille :
Abrial, Jean-Raymond , 1997


4.2 MOOC

 
MOOC on B, Marcel Oliveira, Thierry Lecomte


https://mooc.imd.ufrn.br/course/the-b-method
https://www.atelierb.eu/methode-formelle/enseignement-de-la-methode-b-en-france/
Il contient 20 vidéos pour une durée de 6h50, couvrant les bases de la mé-
thode, depuis la modélisation jusqu'à la gestion de projet. Le site héberge les
modèles utilisés pour les vidéos ainsi que les cahiers de preuve. Le MOOC a
été réalisé en collaboration avec l'Instituto Metropole Digital / UFRN (Natal,
Brésil).


4.3 Exposés

 
Horizon Mathématiques 2024 https://sciencesmaths-paris.fr/horizon-maths-2024
Preuve mathématique et sûreté logicielle Une conférence organisée par la FSMP
sous la coordination scientique d'Hugo Herbelin (Inria, IRIF), le 27 mars 2024 à
l'Institut Henri Poincaré https://fr.wikipedia.org/wiki/Fondation_sciences_
math%C3%A9matiques_de_Paris
"Utilisation des méthodes formelles pour les systèmes critiques, par Thierry
Lecomte (CLEARSY) L'exposé aborde l'utilisation des méthodes formelles pour
assurer la sûreté et la sécurité des infrastructures critiques. Il explique pourquoi
les méthodes formelles sont utilisées, au travers du prisme des activités
industrielles et du retour d'expérience collecté, notamment les accidents qui
surviennent"
https://www.youtube.com/watch?v=Y-3H_7zar9k
"Des méthodes formelles en pratique, par Laurent Voisin (Systerel) Les méthodes formelles fournissent un outil mathématique pour raisonner sur des systèmes informatique, permettant une maitrise accrue des risques. Nous donnerons quelques exemples de cas d'usage à l'échelle industrielle où leur apport est
particulièrement saillant : Conception de système critique, Développement de logiciel critique, validation de données, validation de la spécification d'outils."
Une bibliographie est disponible ici https://blog.systerel.fr/fr/pages/publications/
4

Comments

Post a Comment

Popular posts from this blog

Ce que je dois à Jean-Raymond Abrial

Image
 Quand ai-je découvert Jean-Raymond Abrial ?  Peut-être bien que c'est quand j'ai fait acheter les actes de la conférence de Cargèse et que j'ai lu son article Data Semantics . Ou est-ce lors de la lecture des publications de la DER-IMA d'EDF (située à Clamart) ? Ce qui est sûr c'est que j'ai découvert Z dans le Meyer Baudoin, Méthodes de Programmation chez Eyrolles, puis dans le Delobel Adiba, Bases de données chez Dunod. Quand j'ai débuté en "informatique de gestion" (en I.U.T "Informatique") je trouvais que ce que je lisais était bien peu "scientifique". "Information" "donnée" "rubrique" etc.  Pour "donnée" j'ai appris les théorèmes de Jean-Louis Rigal qui était prof à l'Université Dauphine. Facile : Th1, "Une donnée n'est pas donnée" car c'est le résultat d'une abstraction, Th 2. "Une donnée n'est pas donnée" car une fois donnée, ce n'est...
Read more

Jean-Raymond Abrial (1938, 2025)

Image
  Jean-Raymond Abrial (1938, 2025) Jean-Raymond Abrial est décédé les 26 mai 2025 la vieille de la conférence qui a eu lieu dans le cadre des Journées Scientifiques de l'université de Nantes et qui traitait de ses travaux et de leur mise en oeuvre dans différentes domaines.J.-R Abrial est né en 1938 à Versailles. Après des études au Prytanée militaire de la Flèche, il fera l'Ecole Polytechnique. En 1960 il sera ingénieur du génie maritime. Il sera boursier du gouvernement français à Stanford University puis au Centre de Programmation de la Marine où il travaillera sur une version du langage LTR (Langage Temps Réel). C'est là que Gérard Le Lann, qui a fait partie de l'équipe ayant conçu Internet, l'a connu. J.-R Abrial est pour lui "l'un des plus grands informaticiens français ! Peu enclin à épouser les « modes » qui agitent plus ou moins régulièrement les communautés scientifiques. Liberté de penser, de créer, et liberté d'essaimer !".A Grenoble, d...
Read more

On B, Jean-Raymond Abrial

 Cet article date du temps où Jean-Raymond Abrial habitait rue des plantes à Paris. Digilog était deveni Steria, mais pas encore Clearsy. Donc d'avant 2001. On B Jean-Raymond Abrial Consultant, 26, rue des Plantes, 75014, Paris. abrial@steria.fr In  the B-Book [Abr96], an introduction entitled “What is B ?” presents it in a few pages. There is no point in reproducing this introduction here. There is, however, clearly a need to have in this book a sort of informal presentation of B complementing that of the B-Book for those readers who are not familiar with this approach. This is the purpose of this short text, where the emphasis will be put on the question of the development process with B. At the end of the text, I will also cover some more general problems concerning B (tool, education, research, future). B is o “Debugger”. The aim of B is very practical. Its ambition is to provide to industr...
Read more