Verification of Safety of Aircraft Arrival Procedure using SPIN Model Checker

The volume of air traffic increases dramatically and the air traffic control system is a safety critical system. Failure of the system can cause loss of human life, cost, and hard work of many people. Therefore, the safety of such a system is necessary to prevent these losses. Safety can be ensured by checking the correctness of the system. We address problems related to the safety and correctness of the aircraft arrival procedure. Research exists related to aircraft arrival procedure analysis but according to our knowledge, we do not find its formal verification in SPIN model checker. In this paper, we verify the aircraft arrival procedure by checking specific safety properties on the system. We generate a program graph for the system and give the LTL formula for the safety properties we define on the system. Linear temporal logic (LTL) is used to specify properties in the form of formulas. the model checker takes program graph and LTL formula as input and check whether our system satisfied with LTL formula or not. Verification and result analysis is done using the SPIN model checker. This research is beneficial to ensure correctness of safety critical systems.