Requirements Analysis of Air Traffic Control System Using Formal Methods

Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In this paper formal methods in terms of Z notation is applied for the specification of safety critical system of Air Traffic Control (ATC). Firstly, ATC system model in real world is described. For connectivity of different zones of airspace, the real world ATC system is transformed into a directed graph, which is then used to formalize the major components of formal ATC Model i.e static Topology, Network State, Aircraft and Controller. The whole Formal ATC Model is then presented as encapsulation of formal models of its basic components. Finally, the Formal A TC system Model is checked and analyzed with Z/EVES tool-set.