Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

This report describes work to formalize and validate a specification of the separation minima for aircraft in the North Atlantic (NAT) region completed by researchers at the University of British Columbia in collaboration with Hughes International Airspace Management Systems. Our formal representation of these separation minima is given in a mixture of a tabular style of specification and textual predicate logic. We analyzed the tables for completeness, consistency and symmetry. This report includes the full specification and complete analysis results.  
 
The theory behind our analyis methods can be found in Nancy A. Day, Jeffrey J. Joyce, and Gerry Pelletier, Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region. Lfm97: Fourth NASA Langley Formal Methods Workshop, Hampton, NASA Conference Publication 3356, compiled by C. Michael Holloway and Kelly J. Hayhurst, September 1997.  

Download postscript (786 k) (viewable with recent versions of ghostview) 
Complete tech report in html 
Download PDF 
Bibtex entry 

@TECHREPORT{DaJoPeTR97, 
  title={Formalization and Analysis of the Separation Minima for Aircraft  
         in the North Atlantic: Complete Specification and Analysis Results}, 
  author ={Nancy A. Day and Jeffrey J. Joyce and Gerry Pelletier}, 
  number = {97-12} 
  institution={Department of Computer Science, University of British Columbia}, 
  month={October}, 
  year = 1997,