Archives de l’auteur : ClearSy

System Level Formal (Proof Based) Verification For The CBTC of New York’s line 7 (Flushing)

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.

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 … Continuer la lecture

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 … Continuer la lecture

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 … Continuer la lecture

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 … Continuer la lecture

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, … Continuer la lecture

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 … Continuer la lecture

Publié dans Research, Tools | Un commentaire