Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Aspects of a draft version of the Aeronautical Telecommunications Network (ATN) Standards and Recommended Practices (SARPs) under development by ISO-compliant committees of the International Civil Aviation Organization (ICAO) have been mathematically modelled using a formal description technique. The ATN SARPs are a specification for a global telecommunications network for air traffic control systems. A version of Harel's statecharts formalism embedded within a machine readable typed predicate logic has been used as a formal description technique to construct this mathematical model. Our model has been 'typechecked' to partially validate the internal consistency of the specification. The work described in this paper has already uncovered some problems in the draft SARPs, and will provide a basis for follow-on efforts to apply formal analysis methods such as model-checking and symbolic execution to aspects of the ATN SARPs. The success of this approach suggests that typed predicate logic is useful as a syntactic and semantic foundation for specialized Formal Description Techniques (FDTs).  
 

Presented at FORTE/PSTV'97 (1997 IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification), November, 1997.  
 

@INPROCEEDINGS{AnDaJo97,  
 title={Using a Formal Description Technique to Model Aspects of  
         a Global Air Traffic Telecommunications Network},  
 author ={J. H. Andrews and N. A. Day and J. J. Joyce},  
 booktitle={1997 IFIP TC6/WG6.1 Joint International Conference on  
             Formal Description Techniques for Distributed Systems and  
             Communication Protocols, and Protocol Specification, Testing,  
             and Verification (FORTE/PSTV)},  
  publisher={Chapman and Hall},  
  editors = {T. Higashino and A. Togashi},  
  month={November},  
  year = 1997,  
  note = {To appear}}  
  
Send questions or comments to Nancy Day:  nday@cse.ogi.edu  
 

.