doi: 10.7763/IJET.2012.V4.478
Formal Verification and Validation of Aircraft Departure Process in Air Traffic Control System Using VDM++
Shahid Yousaf
1
,
Nazir Ahmad Zafar
2
,
Sher Afzal khan
3
- 1 Department of Computer Science & IT, The
- 2 the Department of Computer Science, College
- 3 the Department of Computer Science, Abdul Wali
Abstract
The safety critical systems are those whose failure may cause the loss of human life, serious injuries and financial disasters. The air traffic control system (ATC) is a safety critical system and rise in the air traffic volume make it more critical and complex which caused for the unwanted delay in the aircraft departure process. To ensure its safety it requires advance methodologies for its designing process. The VDM++ is an emerging technique based on mathematical notation having object oriented features and used to specify and verify the software system. This technique is used to formalize the departure process of ATC system. The departure process is controlled by the air traffic controllers. The air traffic controllers control the aircraft traffic. This departure process is made possible with the help of the ground and local controller. Initially, the aircraft is under the control of ground controller. Further the control is transfer to the local controller. These both controllers communicate to aircraft and also to each other for safe and secure movement of aircraft and finally the aircraft depart from the airport.
Keywords
- VDM
- VDM++
- ATC
- formal method
How to Cite
Shahid Yousaf, Nazir Ahmad Zafar, and Sher Afzal khan, "Formal Verification and Validation of Aircraft Departure Process in Air Traffic Control System Using VDM++," International Journal of Engineering and Technology, vol. 4, no. 6, pp. 755-759, 2012. https://doi.org/ 10.7763/IJET.2012.V4.478
Copyright & License
Copyright © 2012 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).