Verification Corner, Modeling, refinement, and verification

https://www.youtube.com/watch?v=fSWZWXx5ixc

In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.

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.

Dr Ib Holm Sørensen died January 2012

Nous venons d'apprendre :

http://www.cs.ox.ac.uk/news/448-full.html

Le code du Btoolkit est déposé en ligne.

The source code to the B-Toolkit has been posted 

B-Core no longer supports or maintains the B-Toolkit.

https://github.com/edwardcrichton/BToolkit

Predicate B++

http://www.data-validation.fr/predicateb-a-predicate-animator/

Le site methode-b.com

http://www.methode-b.com/

Brama V0.0.22

http://www.brama.fr/
http://www.brama.fr/index-en.php

"Objective : to put in scene your models developed starting enom the language B."

Brama V0.0.22
Brama is now available in beta version.
Discover this new version.

Formations à l'Atelier B 2014

http://www.atelierb.eu/formation-b/

"Automatisation des preuves pour la vérification des règles de l'Atelier B"

Thèse de doctorat, 23 avril 2013, CNAM, Paris
Mélanie Jacquel
http://cedric.cnam.fr/fichiers/art_2850.pdf

Systerel

http://www.systerel.fr/

http://www.systerel.fr/Formation-a-la-methode-B.html
http://www.systerel.fr/Techniques-de-preuve-en-B.html
http://www.systerel.fr/Approche-B-systeme.html

Atelier B とは？

L'Atelier B est maintenant traduit en japonais
http://www.atelierb.eu/ja/

Atelier B

http://www.atelierb.eu/

Composys

http://www.composys.fr/

User Manual of B Language , Redaction Guide of Mathematic Rules

Deux nouveaux manuels dédiés à l'Atelier B sont désormais disponibles :
- Manuel Utilisateur du Langage B
- Guide de Rédaction de Règles Mathématiques
              
Ces derniers sont actuellement en français et disponibles en open-source (licence Creatice Commons - Paternité). Nous recherchons actuellement des traducteurs souhaitant réaliser
la traduction en anglais de ces 2 documents.
              
Pour participer à ce projet, merci de nous contacter à l'adresse suivante : contact@atelierb.eu.
Bien cordialement
CLEARSY SYSTEM ENGINEERING
Spécialiste des Systèmes Sécuritaires
              
              
Dear Users,
              
Two new manuals dedicated to Atelier B are now available :
              
User Manual of B Language
Redaction Guide of Mathematic Rules
              
              
These manuals are available in french and released as open-souce (License Creative Commons - Attribution). We are currently searching for translators wishing to
contribute to english translation of these 2 documents.
              
To participate to this work, please contact us: contact@atelierb.eu.
Best Regards
CLEARSY SYSTEM ENGINEERING
Specialist in Safety Critical Systems

Atelier B or Atelier B ?

What's in a name?

http://atelier-b.blogspot.com/
http://www.atelierb.eu/html/liens.html

The beta 2 version of Atelier B 4.0

              
Starting with the launch of the beta 2
 version of Atelier B 4.0, which is
now available at no cost on the Atelier
 B site in order to collect opinions
and comments, then finalize a stable
 version by the end of January 2009.
         

Atelier B for free (web site of Clearsy)

News

Atelier B 4.0 is available in beta test (22/08/2008)

ClearSy make it available to users for get feedback on this version. We thank in advance all the users who contribute to the improvement of this new version. Windows (10Mo) Linux (30Mo) Mac OS (28Mo) To contact us and send your comments and suggestions, contact us at: contact@atelierb.eu More informations about Atelier B 4.0...