Applying a Formal Method in Industry: a 25-Year Trajectory
This work provides insights for industry practitioners and academics on overcoming barriers to adopting formal methods in safety-critical domains, though it is incremental in summarizing long-term experience.
The paper examines the 25-year application of formal methods (B and Event-B) in industries like railways, smartcard, and automotive, addressing challenges such as lack of understanding and integration issues, and highlights the added value and future prospects for safety-critical systems.
Industrial applications involving formal methods are still exceptions to the general rule. Lack of understanding, employees without proper education, difficulty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. Hence the feedback provided by industry to academics is not as constructive as it might be. Summarizing a 25-year return of experience in the effective application of a formal method - namely B and Event-B - in diverse application domains (railways, smartcard, automotive), this article makes clear why and where formal methods have been applied, explains the added value obtained so far, and tries to anticipate the future of these two formalisms for safety critical systems.