Formal Verification of Aircraft Departure Procedure Using Spin Model Checker

The volume of air traffic increase dramatically and safety of air traffic systems are becoming critical issue day by day. Failure of system can cause loss of human life, cost and hard work of many peoples. Therefore, safety of such system is necessary to prevent these loses. Safety can be ensured by checking correctness of the system. We address problem related to ensuring safety and correctness of the aircraft departure procedure using SPIN. Research exists related to aircraft departure procedure analysis but according to our knowledge we do not find its formal verification in SPIN model checker. In this paper, we verify aircraft departure procedure by checking specific safety properties on the system. We generate program graph for system and give LTL formula for safety properties we define on the system. Linear temprol logic (LTL) is use to specify properties in the form of formula. Model checker take 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 SPIN model checker. This research is beneficial to ensure correctness of safety critical systems.