Spécifier ou comment maîtriser l'abstrait

J.R. Abrial 
Spécifier ou comment maîtriser l'abstrait, 
TSI, Vol 3, N° 3, 
1984, 
pp. 201-219

Introduction à la méthode B, J.R. Abrial, vidéogrammes

http://data.bnf.fr/documents-by-rdt/13489775/3170/page1

• Introduction à la méthode B 5

  Description matérielle : 1 cass. vidéo (13 min environ) : 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

  [catalogue]
  
• Introduction à la méthode B 4

  Description matérielle : 1 cass. vidéo (13 min environ) : 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

  [catalogue]
  
• Introduction à la méthode B 2

  Description matérielle : 1 cass. vidéo (13 min environ) : 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

  [catalogue]
  
• Introduction à la méthode B 1

  Description matérielle : 1 cass. vidéo (13 min) : 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

  [catalogue]
  
• Introduction à la méthode B 3

  Description matérielle : 1 cass. vidéo (13 min environ) : 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

  [catalogue]
  
• Introduction à la méthode B 6

  Description matérielle : 1 cass. vidéo (13 min environ) : 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

  [catalogue]
• 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 (cop.)
  [catalogue]

Code Generation for Event-B

http://arxiv.org/pdf/1602.02004.pdf

Universidade da Madeira Centro de Ciencias Exactas e da Engenharia 

PhD THESIS presented in fulfilment of the requirement for the degree of Doctor of Philosophy 

Major: Software Engineering 

Code Generation for Event-B 

presented by V´ICTOR ALFONSO RIVERA ZU´ NIGA ˜ 

supervised by NESTOR CATA ´ NO COLLAZOS ˜ June 2014 

Abstract Stepwise refinement and Design-by-Contract are two formal approaches for modelling systems. These approaches are widely used in the development of systems. Both approaches have (dis-)advantages: in stepwise refinement a model starts with an abstraction of the system and more details are added through refinements. Each refinement must be provably consistent with the previous one. Hence, reasoning about abstract models is possible. A high level of expertise is necessary in mathematics to have a good command of the underlying languages, techniques and tools, making this approach less popular. Design-by-Contract, on the other hand, works on the program rather than the program model, so developers in the software industry are more likely to have expertise in it. However, the benefit of reasoning over more abstract models is lost. A question arises: is it possible to combine both approaches in the development of systems, providing the user with the benefits of both? This thesis answers this question by translating the stepwise refinement method with EventB to Design-by-Contract with Java and JML, so users can take full advantage of both formal approaches without losing their benefits. This thesis presents a set of syntactic rules that translates Event-B to JML-annotated Java code. It also presents the implementation of the syntactic rules as the EventB2Java tool. We used EventB2Java to translate several Event-B models. The tool generated JML-annotated Java code for all the considered Event-B models that serve as final implementation. We also used EventB2Java for the development of two software applications. Additionally, we compared EventB2Java against two other tools that also generate Java code from Event-B models. EventB2- Java enables users to start the software development process in Event-B, where users can model the system and prove its consistency, to then transition to JML-annotated Java code, where users can continue the development process. Key Words— Modelling system by stepwise refinement, Event-B, Designby-Contract, Java, JML, EventB2Java

Software Specification Methods, An Overview Using a Case Study

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, P. Poizat and M. Frappier.

Programming as a Mathematical Exercise

http://rsta.royalsocietypublishing.org/content/312/1522/447

Programming as a Mathematical Exercise [and Discussion]

J. R. Abrial, J. C. Shepherdson, J. S. Hillmore, R. L. Constable

Published 1 October 1984.DOI: 10.1098/rsta.1984.0070

ABZ 2016

http://www.cdcc.faw.jku.at/ABZ2016/

ABZ 2016

ASM, Alloy, B, TLA, VDM, Z

May 23-27, 2016

Linz, Austria

Accepted Papers

http://www.cdcc.faw.jku.at/ABZ2016/accepted/

Conception d'algorithmes

Conception d'algorithmes

Principes et 150 exercices corrigés

• Auteur(s) : Patrick Bosc, Marc Guyomard,Laurent Miclet
• Editeur(s) : Eyrolles
• Collection : Algorithmes

• Nombre de pages : 818 pages
• Date de parution : 25/02/2016 
• EAN13 : 9782212133660

La conception des algorithmes : une science !

L'algorithmique est l'art et la science de concevoir des algorithmes corrects et efficaces. Pour beaucoup d'informaticiens, c'est l'aspect artistique qui prédomine : on cherche l'idée lumineuse, la structure cachée, la réponse astucieuse. Mais la conception des algorithmes est d'abord une science dont il faut posséder les bases et les techniques avant d'exprimer sa créativité. Ce livre invite le lecteur à une approche rigoureuse de la construction d'algorithmes. Il explique comment la même idée peut se retrouver dans plusieurs algorithmes correspondant à des problèmes différents. Il donne les outils pour analyser rationnellement un problème, le classer dans une famille de méthodes et produire une solution exacte.

Un manuel de référence sur la construction raisonnée des algorithmes

Dans chaque chapitre de ce livre, les bases théoriques et techniques sont rappelées et illustrées par des exemples. On y trouve ensuite un grand nombre d'exercices, accompagnés d'une correction minutieuse et complète. De la sorte, on y voit comment une démarche rationnelle permet d'atteindre une solution, exacte par construction, à travers une grande variété de cas. Après des rappels sur le raisonnement, les structures de données et la complexité, le livre parcourt les grandes méthodes de construction d'algorithmes : invariants, récursivité, essais successifs, méthodes PSEP, algorithmes gloutons, diviser pour régner, programmation dynamique. Au total, près de 150 exemples d'algorithmes sont ainsi analysés et construits rigoureusement.

http://www.editions-eyrolles.com/Livre/9782212133660/conception-d-algorithmes#complement

Machines virtuelles pour le B événementiel

http://www.researchgate.net/publication/228364789_Machines_virtuelles_pour_le_B_vnementiel

Jean-Raymond Abrial at ICTAC 2015

http://www.ictac2015.co/http://www.ictac2015.co/

One ot the invited speakers :

Jean-Raymond Abrial

Consultant (France)

Jean-Raymond Abrial is a French computer scientist, widely known as the co-inventor of various formal approaches to software specification: Z, B and Event-B.

He is the author of the "B-book" (Cambridge University Press, 1996), which presents the B-Method. More recently, he published the book "Modeling in Event-B: System and Software Engineering" (Cambridge University Press 2010). He was Guest Professor at ETH Zurich from 2004 to 2007, where he led the team developing the Rodin Platform tool for Event-B (funded by the European Project "Rodin"). After that, he was a researcher, also at ETH Zurich, working on the European Project "Deploy" until May 2009.

Jean-Raymond Abrial has been invited to give courses on formal methods in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before Zurich, he was a consultant for more than 20 years working in close contact with several industrial companies and universities around the world.

ABZ 2016

http://www.cdcc.faw.jku.at/ABZ2016/call4papers/

The ABZ conference is dedicated to the cross-fertilization of six related state-based and machine-based formal methods, Abstract State Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. It builds on the success of the first ABZ conference held in London in 2008, where the ASM, B and Z conference series merged into a single event, the second ABZ 2010 conference held in Orford (Canada), where the Alloy community joined the event, the ABZ 2012 held in Pisa (Italy), which saw the inclusion of the VDM community, and ABZ 2014 held in Toulouse (France), which brought the inclusion of the TLA community into the ABZ conference series. The ABZ 2016 conference will be held in Linz, Austria.

Contributions are solicited on all aspects of the theory and applications of ASMs, Alloy, B, TLA, VDM, Z approaches in software/hardware engineering, including the development of tools and industrial applications. The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods and tools that are distinguished by mathematical rigor and have proved to be industrially viable. The main goal of the conference is to contribute to the integration of accurate state- and machine-based system development methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation, mathematical verification of reliable high-quality hardware/software systems.

Although organized to host several formal methods with ASM, Alloy, B, TLA, VDM and Z, in a single event, editorial control of the joint conference is vested in one integrated program committee, which will respectively determine its ASM, Alloy, B, TLA, VDM and Z content, to be presented in parallel conference tracks with a schedule to allow the participants to switch between the sessions.

As successfully practiced at ABZ 2014, the 5th edition of ABZ will include again special sessions dedicated to a shared real-life case study among all the methods addressed in ABZ 2016. The objective of this session is to enrich the set of case studies developed with ABZ methods with a practical and real-life case study. After the success of the “Landing Gear” case study at ABZ 2014 in the aeronautical context this time the organizers defined a real-life case study issued from the medical domain with challenging safety requirements. The ABZ 2016 case study emphasizes the control of a hemodialysis machine. See http://www.cdcc.faw.jku.at/ ABZ2016/HD-CaseStudy.pdf for a detailed description of this case study.

Submission of Papers

Proposals are invited for workshops and tutorials to take place before the main conference.

Four kinds of contributions are invited:

• Research papers: full papers of not more than 14 pages in LNCS format, which have to be original, unpublished and not submitted elsewhere.
• Short presentations of work in progress, and tool demonstrations. This is an excellent opportunity for Ph.D. students to present and validate their work in progress. An extended abstract of not more than 4 pages is expected and will be reviewed.
• Answers to case study papers: full papers of not more than 14 pages in LNCS format reporting on the experiments conducted with any of the state based techniques in the scope of ABZ 2016.
• Application in industry papers reporting on work or experiences on the application of state based formal methods in industry. An extended abstract of not more than 4 pages is expected and will be reviewed. It is also an interesting option for industrial practitioners who sometimes face too many constraints to prepare a full paper.

Contributions should be submitted electronically in PDF at the ABZ 2016 conference submission website (Easy Chair).

The papers must be prepared using the SPRINGER LNCS style. The answers to case study should be submitted electronically in PDF at the ABZ 2016 case study submission website (Easy Chair)".

All research and short accepted papers will be published in a volume of Springer's LNCS series. The answers to case study papers and the application in industry papers will be published in a volume of Springer's CCIS series. The two volumes will be distributed at the conference.

Journal Special Issues

It is planned that an improved version of a selected number of contributions will be published in a special issue of the journal Science of Computer Programming for the research papers and in a special issue of the Software Tools and Technology Transfer journal for the answers to case study papers (to be confirmed).

Workshop Proposals

Workshops and tutorials will be associated to the main event ABZ. Proposals are solicited in areas related to the conference topics. Workshop proposal should be sent to the workshop chairs.

The deadline for submissions is October 16, 2015. Notifications will be sent by November 6, 2015.

Tutorial Proposals

Tutorial proposal should be sent to the tutorial chairs.

The deadline for submissions is February 15, 2016. Notifications will be sent by March 14, 2016.

Important Dates

Research paper and answers to case study submission:	January 15, 2016
Short paper submission:	February 04, 2016
Workshop proposal submissions:	October 16, 2015
Workshop proposal notifications:	November 06, 2015
Tutorial proposal submissions:	February 15, 2016
Acceptance notification:	February 22, 2016
Tutorial proposal notifications:	March 14, 2016
Final Version due:	March 14, 2016
Main ABZ 2016 conference:	May 23-27, 2016

Program Committee Chairs

• Michael BUTLER, University of Southampton, Southampton, UK
• Klaus-Dieter SCHEWE, Johannes-Kepler-Universität Linz and Software Competence Center Hagenberg, Linz/Hagenberg, Austria

Case Study Chairs

• Atif Mashkoor, Software Competence Center Hagenberg, Hagenberg, Austria (atif.mashkoor@scch.at)
• Miklos Biro, Software Competence Center Hagenberg, Hagenberg, Austria (miklos.biro@scch.at)

Tutorial Chairs

• Vincenzo Gervasi, Università di Pisa, Pisa, Italy (gervasi@di.unipi.it)
• Michael Leuschel, Universität Düsseldorf, Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)

Workshop Chairs

• Yamine Ait-Ameur, Institut National Polytechnique de Toulouse, France (yamine@enseeiht.fr)
• Stephan Merz, INRIA Nancy, Nancy, France (stephan.merz@loria.fr)
• Alexander Raschke, Universität Ulm, Ulm, Germany (alexander.raschke@uni-ulm.de)

Program Committee

Program committee will be announced at a later date.

Conference Organizers

• Klaus-Dieter SCHEWE, Johannes-Kepler-Universität Linz and Software Competence Center Hagenberg, Linz/Hagenberg, Austria (Klaus-Dieter.Schewe@scch.at)
• Atif Mashkoor, Software Competence Center Hagenberg, Hagenberg, Austria (atif.mashkoor@scch.at)
• Mariam Rady, Johannes-Kepler-Universität Linz (m.rady@cdcc.faw.jku.at)
• Mircea Boris VLEJU (webmaster), Johannes-Kepler-Universität Linz (b.vleju@cdcc.faw.jku.at)
• Martina Höller, Software Competence Center Hagenberg, Hagenberg, Austria (martina.hoeller@scch.at)

For questions concerning ABZ 2016, contact Klaus-Dieter SCHEWE (Klaus-Dieter.Schewe@scch.at).