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.
Email: [email protected]; [email protected]; [email protected];[email protected]
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
