Formal verification of software safety criteria using Event-B

Software safety criteria plays a very important role in verifying software safety, and it offers the target when we carry out safety analysis. However, the software criteria has not been widely applied, because the description in natural language may be semantically vague and the manual verification brings huge workload. Formal methods can just make up the above weakness because of its rigorous logic and automatic verification. Event-B is a kind of formal method, which has a support tool RODIN. In this paper, we formalize and verify the software safety criteria in Event-B, and propose implementation process. Through this implementation, the safety criteria can be verified automatically. At last, a landing gear retraction system is applied to verify the availability of this method.