Modeling And Formal Specification Of Air Traffic Control System Using Z Notation

Abstract

In this paper, an abstract Air Traffic Control (ATC) System is modeled using Formal Methods, in terms of Z-notation. ATC system is a highly distributed and safety critical system. For modeling of distributed nature of ATC system, a separate queue of flying aircrafts is maintained at each controlled airspace. To ensure safety, it is mandated that each airspace and runway do not exceed its capacity limit in all state operations. Firstly, Requirements Analysis is done using UML diagrams and then the Formal ATC system Model is described by Z-notation. Finally, the Formal ATC system Model is checked and analyzed with Z/EVES tool-set.