B Method for the specification and fabrication of software and proven critical systems

There has been a significant increase in the complexity of software over the last decades, notably regarding safety requirement levels, overall coherence and the interaction between components. A profusion of methods based upon model verification or static analysis currently allows improvement in the fiability of critical software. Although it has shown some limitations, the B method stands out from others in many aspects. Its main force is undoubtfully the use of a programming language which ensures that each step is verified through mathematical evidence. Altough rigour and precision are assisted on in the writing process, the integration of quality as early on as in the designing stage remains a significant asset.