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...

Full description

Saved in:
Bibliographic Details
Main Authors: Jamal, M., Zafar, N.A.
Format: Conference Proceeding
Language:English
Subjects:
Air safety
Air traffic control
Aircraft
Computer errors
Computer science
Error correction
Graph theory
Humans
Information analysis
Network topology
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/ICIET.2007.4381340