Formal Reasoning for Air Traffic Control System Using Event-B Method

We present a formal modeling and verification of Air Traffic Control system (ATC) for airspace management. This system assists air traffic controllers by visualizing aircrafts in the airport vicinity. In such a critical-safety system, the use of robust formal methods that assure bugs absence is highly required. Therefore, we use a formalism of discrete transition systems based on abstraction and refinement along proof obligations. These proofs ensure the consistency of the system by mean of invariants preservation and deadlock freedom. The first guarantee that all invariants hold permanently and thus provide a handy solution for bugs absence verification. The second prove that the system runs forever to avoid deadlock. This modeling and proving enable us to establish that the system is, relatively to some criteria, correct by construction.