Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region

• Main Authors: Nancy A. Day, Jeffrey J. Joyce, Gerry Pelletier
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: 1997
• Subjects: North Atlantic
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7227; http://www.intrepid-cs.com/publications/papers/lfm97.pdf

The formalization and analysis of an air traffic control separation minima serves in this paper as an illustration of an approach that uses formal operational semantics to drive the automated analysis of specifications. This contrasts with the approach of translating one notation into the input format for an analysis tool, or hard-coding the semantics of a particular notation into the implementation of an analysis technique. The semantic functions capture the structure of the specification and can be directly evaluated to map a notation to a rigourous mathematical foundation. This work contributes to a greater appreciation of how the structure of a specification (e.g., the organization of a table), not just the semantics, is an important input to many analysis functions. Building upon a common mathematical foundation, different notations can be combined to support an integrated approach to the analysis of a formal specification. A related issue is the importance of being able to rever.