Design and Conformance of Air-Traffic Control
Overview
NSF Award Abstract - #0086154
ITR: Design Conformance Software
The proposed research will investigate new software engineering techniques and tools for infrastructural software that will improve its reliability, safety, and predictability. The key idea is to use abstract design models to drive new static analyses that check that the software correctly implements its design (and if not, identify the source of the problem). To ensure that our research addresses the important issues that developers face in the field, we will conduct our research in the context of the development of an air traffic control system component. Specifically, the research will investigate the use of object models to express important design properties and new pointer analysis algorithms to verify that the code correctly implements the object models. Object models describe essential object in the heap and the relationships between them; pointer analysis automatically analyzes code to extract information about how objects refer to each other. The research will investigate techniques that improve the precision of the pointer analysis by using the object model to focus the analysis on the properties of interest.
Air-Traffic Control and the Direct-To System*
The capacity of the national air traffic control (ATC)
system is not keeping pace with the high growth in flights and air travelers.
NASA is performing research and development of a suite of tools that will
help improve the efficiency of the ATC system, by providing automation
assistance to air traffic controllers. The suite of tools is known
as the Center-TRACON Automation System, or CTAS. Some CTAS tools are
already in operation at several major airports, including DFW and LAX.
One new tool in the CTAS suite is the Direct-To Tool (D2).
D2 enables aircrafts to shorten their flights by skipping unnecessary flight
segments. It tells controllers which segments can be skipped and
whether there will be conflicts with other aircrafts along the new, shorter
path. NASA and the FAA plan to move toward
preparing the software for deployment into the FAA infrastructure at all
sites where benefits would be seen, once the benefits of D2 are proven.
As part of this preparation,
a critical portion of the software needs to be redesigned to improve maintainability,
performance, and robustness.
Specification of the D2 System
We describe
the requirements of D2 and
build object models for it. These object models
together with D2's specification will help in its analysis and redesign.
We give a
low-level specification of D2 (in Alloy),
that is close to the
actual design of the system. In order to facilitate redesign, we present a
high-level specification
(in Alloy Alpha) that encompasses the air-traffic control problem.
The latter will help us put appropriate boundaries around the D2 problem, thereby
allowing us to develop correctness criteria, and improved design.
* Text taken from Software Design Workshop general information.