Archives de catégorie : Applications
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.
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
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
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
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.