Following our post “Event-B to demonstrate metro safety in New York“, a presentation of
the final results of the project have been presented in Paris on June 26th.
System Level Formal (Proof Based) Verification For The CBTC of New York’s line 7 (Flushing)
Publié dans Applications, Event
Laisser un commentaire
B Solutions to some VSTTE Competition Problems Released
Several software verification competitions have been organized last years, Some problems from these competitions have been selected and solved using the B method. For each of these problems, are provided a B model archive, a report and source code.with different objectives and modalities.
Publié dans Applications
Laisser un commentaire
Three kinds of projects
Atelier B 4.1 supports three different kinds of projects:
- software project: using B language, aimed at producing C or Ada code.
- system level project: using Event-B language, aimed at producing evidences that a system level specification is sound and at preparing software development.
- data validation project: using B or Event B language, aimed at verifiying that constants can be valued. This applies for large set of constants and related properties.
The figure below draws a picture of the possible connections between these projects.
Publié dans Applications
Laisser un commentaire
Atelier B Open Source Tools Map
At the occasion of the forthcoming Atelier B 4.1 release, a map referencing the open-source projects is published.
All the open-source tools are hosted on Sourceforge facilities.
Publié dans Tools
2 commentaires
BWare: a new project on proving B proof obligations
BWare, a new research project related to the B method has started in September 2012. It is funded for a period of 4 years by the programme “Ingénierie Numérique & Sécurité” of the French national agency ANR.
This project is aimed at providing a mechanized framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method. The methodology used in this project will consist in building a generic platform of verification relying on different theorem provers, such as first-order provers and SMT solvers. Beyond the multi-tool aspect of this methodology, the originality of the BWare project also resides in the requirement for the verification tools to produce proof objects, which are to be checked independently.
The BWare consortium associates several academics entities (Cedric, LRI, and Inria) and industrial partners (Mitsubishi Electric R&D Centre Europe, ClearSy, and OCamlPro).
For further information, you can refer to the website of the project: http://bware.lri.fr/
Publié dans Research
Laisser un commentaire
Metros and Trains equipped with B software – Updated map
Publié dans Applications
Laisser un commentaire
Bug Status Section Updated
With the forcoming Atelier B 4.1 Community Edition (to be released in September 2012), the Bug Status section has been updated.
Publié dans Tools
Laisser un commentaire
Event-B to demonstrate metro safety in New York
The New York City Transit authority (NYCT) decided to include formal proofs at system 
level as part of the safety assessment for the New York City subway Line 7 (Flushing) modernization project. Event-B and Atelier B are used to complete the formal demonstration of the safety case in two years.
Publié dans Applications
Laisser un commentaire
Atelier B 4.x at Reliable Software Workshop (Paris)
The Journées sur la Fiabilité du Logiciel organized on June 14-15, 2012 by the Initiative de Recherche et Innovation sur le Logiciel Libre and the Groupe Thématique Logiciel Libre du pôle System@tic adress validation, certification, proof and code analysis. 
At this occasion, Atelier B and its applications will be presented.
Publié dans Event, Tools
2 commentaires
Why3 as another proof toolchain for Atelier B
In 2011, Why3 proof tool-chain has been plugged into Atelier B, in order to transform Proof Obligations generated by Atelier B into Why3 verification conditions. 
Those verification conditions can then be checked with several automatic provers (Alt-Ergo, CVC3 and Z3). Overall, the automatic provers of Why3 proof tool-chain prove more proof obligations that native Atelier B automatic prover (F0 and F1). An article on this topic has been accepted at ABZ 2012 conference.
Publié dans Research, Tools
Un commentaire