The seminar, entitled “Proven software with B executing on Low Cost High integrity Platform”, is aimed at presenting the latest innovations concerning the use of the B formal method for the development of safety critical systems:
“Atelier B has been heavily used in industry, mainly in the railways, for the development of proven safety critical software. The automatic pilot (80 kloc) of METEOR metro line 14 in Paris, fully proved in B and still no bug found since 1998, is the best example of this technology used today in more than 25% of worldwide automatic metros. Over the time, several new modelling techniques and their related tools have appeared, aimed at shortening development time as well as validation-by-proof effort. Automatic refinement, proof integrated to model edition and abstract model edition are new features that are being deployed on critical systems. More recently, a new secured architecture, based on two processors and combining software (B formal method) and hardware techniques compatible with EN5012{6, 8, 9} standards, has emerged. This execution platform has been deployed in several certified railway applications (Sao Paulo metro, Stockholm metro). It has been selected for a french collaborative R&D project to obtain a generic product able to seamlessly generate SIL4 applications. Code generation and validation-by proof will be completely automated. The related IDE will accept any Domain Specific Language through a public API. During the seminar, modern B development techniques and low cost high integrity platform will be detailed.”