Formal modeling of ATC signals using Z notation

The light signals play a vital role in the management of traffic systems. They are the key component of traffic control systems, which properly channelize the traffic flow. Therefore, the area of air traffic control (ATC) signals also becomes critical concerning the movement of airplanes because a failure in ATC light signal could cause the loss of human life and financial disasters. The air traffic control is a safety critical system and failure in such systems is not affordable. In this paper we have developed the formal model of ATC light signals where different light signals of the model are formally specified using Z-notation. Our proposed model ensures the correspondence between the functional behavior of the light signal communication system and its functional requirements. Moreover, the system also becomes important due to its uniqueness since it has an extra number of control signal combinations as compared to ordinary signal systems.