Formal Analysis a
Formal Analysis and verification of Arrival Procedure for an Aircraft using Petri nets
Ayesha Sadiq1, 2, Farooq Ahmad1, Tabbasum Naz2, Humera Faisal2
1Faculty of Information Technology, University of Central Punjab, Lahore, Pakistan
2Department of Computer Science, COMSATS University of Information Technology, Lahore, Pakistan.
Abstract: Air Traffic Control (ATC) is safety critical real times service in Air Traffic Management (ATM) where system correctness is a major concern, and which requires high degree of confidence and targets zero failure rates to avoid loss of human lives and other disastrous (unfavorable) conditions. The ever increasing volume of air traffic may cause unwanted delays in the flight during the arrival procedure of the aircrafts. Hence, there is an absolute need to formally model and verify the arrival procedure of the aircrafts to avoid delays and to assure the controlled coordination between aircraft and air traffic controllers which are involved in this process. In this paper, we have modeled the arrival procedure of the aircraft using Petri nets which have been used traditionally as a rationale for formal specification and verification for such a safety critical systems. The proposed model assures how the behavior of acting objects affects the overall procedure of arrival management. Moreover, we have verified the proposed model using coverability tree as an analysis method that ensures the deadlock-freeness and reliability of the mechanism involved between the aircraft and the air traffic controllers (ramp controllers and ground controllers) for the arrival of the aircraft.
[Ayesha Sadiq, Farooq Ahmad, Tabbasum Naz, Humera Faisal. Formal Analysis and verification of Arrival Procedure of an Aircraft using Petri nets. J Am Sci 2013;9(3):221-228]. (ISSN: 1545-1003).http://www.jofamericanscience.org. 30
Keywords: Petri net analysis and verification; ATC; aircraft arrival; formal modeling. Full Text 30