Application of Software Safety Analysis Using Event-B

Event-B is a formal method for modeling systems based on first order logic and set theory, which has gained widespread attention. Software safety analysis techniques have played important roles in improving and verifying the safety of software intensive systems. Event-B language and its tool support can be used for software safety analysis, for systems either modeled in Event-B or developed in other ways, in particular for safety critical systems. The case study outlined in this paper is aimed at applying software safety analysis based on Event-B to a landing gear extend and retract system. Firstly, the mechanism of Event-B for software safety analysis is discussed, including theorem proving, model checking and animation, which are complementary for each other. Then, the procedure of safety analysis using Event-B is presented. The case study shows that it can provide systematic approaches to identifying defects and weak links in software systems.