Archives de catégorie : Applications

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

Metros and Trains equipped with B software – Updated map

Publié dans Applications | 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

Port & development of Brama model animator to Atelier B

Atelier B 4.0 natively supporting event B, animating such models is mandatory.  The Brama  animator has been ported on Atelier B 4.0 environment: the predicateB predicate evaluator has been ported to C++ and connected with B-Compiler.

Publié dans Applications, Tools | Laisser un commentaire