Using
a Formal Description Technique to Model Aspects of a Global Air Traffic
Telecommunications Network
presented by
Jamie Andrews
| |
Using
a Formal Description Technique to Model Aspects of a Global Air Traffic
Telecommunications Network
presented by
Jamie Andrews
|
| formalWARE
project
formalWARE
formalWARE
|
Presented by James H. Andrews
at the 10th annual FORTE/PSTV conference
held in Osaka, Japan on Nov.
18-21.
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). Presentation (PDF) Presentation (Thumbnails) Presented at FORTE/PSTV'97
(1997 IFIP TC6/WG6.1 Joint International Conference on Formal Description
Techniques for Distributed Systems and Communication Protocols, and Protocal
Specification, Testing, and Verification), Osaka, Japan, November 18-21,
1997
. |
