| Example One:
Aeronautical Telecommunications Network Specification
What is ATN?
The Aeronautical Telecommunications Network
(ATN) is a global telecommunications network for air traffic control systems.
The ATN Standards and Recommended Practices (SARPs) is a specification
of this system. Some of the source documents used for this study
were accessed via FTP from ftp.stel.com.
What did formalWARE do with the ATN
specification?
This application of formal methods involved
creating a formal specification of the ISO-proposed Aeronautical
Telecommunications Network (ATN). The specification is expressed in terms
of statecharts and the S language. Click here to view an abstract
of this work.
What methods did formalWARE use?
Following an approach under development
by Nancy Day (UBC Computer Science) in her Ph.D. thesis research, this
application involves the textual representation of Statecharts derived
from the contents of the ATN SARPs. This textual representation of Statecharts
is embedded in the S notation. In an effort led by Dr. Jamie Andrews (UBC
Computer Science), project members from both UBC and UVic contributed to
the derivation of the Statecharts models from the ATN SARPs. Hughes personnel
assisted university based researchers by answering questions about the
interpretation of various aspects of the ATN SARPs. This effort was motivated
by earlier work at Hughes on using Day's approach to Statechart specification
to formalize aspects of the ATN SARPs.
In follow-on work, Dilian Gurov (UVic Computer
Science) is investigating the use of a notation called CSS
with a supporting tool called the "Concurrency Workbench" to validate aspects
of the ATN SARPs. Nancy Day is also investigating the application of tool-assisted
analysis techniques to the ATN SARPs in the context of her Ph.D. thesis
research. |
