The release of Atelier B 4.7 materializes two decades of industrial exploitation of the B formal method, with the support of 24 collaborative R&D projects for various topics such as formal data validation, safe program execution, mathematical proof, automated model refinement or VHDL generation.
Here are some significant metrics:
- More than 1 century.man for its development until now
- Bug-free generated software for more than 20 years of operation
- Guaranteed emergency braking for more than 30% of the world’s automatic metros and for several tens of billions of cumulative passengers
- Formally proven security policies for microcircuits in tens of millions of smart cards worldwide
- Safe opening of platform screen doors for the transit of billions of passengers