Home Page
Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic
 
by Nancy A. Day, Jeffrey J. Joyce and Gerry Pelletier 
 
formalWARE 
    project  

  Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

 Abstract  
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 reverse the effect of the semantic functions so that analysis results are provided to users at the same level of abstraction used in the input specifications.  

The formalization of the separation minima combines the use of a tabular style of specification with predicate logic. This paper discusses how automated analysis functions were applied to the specification to check for the properties of consistency, completeness and symmetry. The benefit of doing this analysis is demonstrated by the discovery of an ambiguity in the separation minima. 


Download gzipped postscript(viewable with recent versions of ghostview) 
Download PDF 
Bibtex entry 
 
Presented at The Fourth NASA Langley Formal Methods Workshop, 10-12 September 1997, Hampton, Virginia, USA.  

 

Bibtex Entry 
 

@INPROCEEDINGS{DaJoPe97, 
  title={Formalization and Analysis of the Separation Minima for Aircraft  
         in the North Atlantic}, 
  author ={Nancy A. Day and Jeffrey J. Joyce and Gerry Pelletier}, 
  booktitle={Lfm97: Fourth NASA Langley Formal Methods Workshop}, 
  publisher={NASA Conference Publication 3356}, 
  editors = {C. Michael Holloway and Kelly J. Hayhurst}, 
  month={September}, 
  year = 1997, 
  note = {To appear}} 
 

Send questions or comments to Nancy Day at: day@cs.ubc.ca