Event-B based modeling for landing gear extend and retract control system

The control system has become more and more complex with an increasing demanding of dependability. Sometimes we want to know whether the system is what exactly we want. The use of formal modeling methods and refinement shows a great potential in solving this problem. In this paper, we proposed an modeling method for control system based on Event-B. Through preprocessing of requirements we can facilitate and guide our modeling. With Rodin platform we instantiate the method using the landing gear control system. The use of invariants as safety constraints and animation helps to complete the verification process. This method not only makes formal modeling easy and approachable, but also helps us find some of the missing requirements.