formalWARE
project
Participating
Organizations
Research
Topics
People
formalWARE
results
Overview
Publications
Presentations
Tools
Methods
Examples
Training
formalWARE
information
Events
Index
Links
Contacts |
Example Two:
North Atlantic Separation Minima Specification and Analysis
What is the “Separation Minima” for
NAT?
| This example is based on
the third edition (effective December 1992) of a document titled "Application
of Separation Minima (North Atlantic Region)", a specification published
by Transport Canada on behalf of the International Civil Aviation Organization
(ICAO) (http://www.CAM.ORG/~icao/). |
 |
The separation minima provides guidance to
air traffic controllers managing the region of oceanic airspace between
Europe and North America. It is also used as the basis for the development
of software based systems that support the management of air traffic in
the NAT region.
What did formalWARE do with the “separation
minima” specification?
This application of formal methods involved
the formalization of the separation minima based on a description provided
in a source document.
What methods did formalWARE use?
As part of her Ph.D. thesis research,
Nancy Day, has developed a tabular style of specification that can be integrated
with the S notation. In collaboration with Hughes personnel, she used this
style of specification to create formal representations of predicates and
functions which collectively specify the minimum required separation (given
as either a measurement of distance, degrees of latitude, or time) between
aircraft operating in the NAT region. MDA personnel also contributed to
early stages of this work. In addition to developing a formal representation
of this separation minima, Day has used this application to motivate development
of a software tool which performs several automated analysis functions
such as "completeness checking".
The results of this work are presented
in "Formalization and Analysis
of the Separation Minima for Aircraft in the North Atlantic Region"
and " Formalization and Analysis
of the Separation Minima for Aircraft in the North Atlantic Region: Complete
Specifications and Analysis Results."
Please also see Nancy's presentation
at the NASA Langley Formal Methods Workshop. |
