production models that we have examined, very few counterexamples are
longer than a few steps.
case studies
To be of any real value, model checking must be able to handle much larger problems. Three case studies on the
application of our tools to industrial
examples are described here. A fourth
case study is discussed in Miller et al. 7
ADGS-2100 Window Manager. One of
the largest and most successful applications of our tools was to the ADGS-
2100 Adaptive Display and Guidance
System Window Manager. 13 In modern
aircraft, pilots are provided aircraft
status primarily through computerized display panels similar to those
shown in Figure 3. The ADGS-2100 is
a Rockwell Collins product that provides the heads-down and heads-up
displays and display management
software for next-generation commercial aircraft.
The Window Manager (WM) ensures
that data from different applications is
routed to the correct display panel. In
normal operation, the WM determines
which applications are being displayed
in response to the pilot selections.
However, in the case of a component
failure, the WM also decides which in-
formation is most critical and routes
this information from one of the re-
dundant sources to the most appropri-
ate display panel. The WM is essential
to the safe flight of the aircraft. If the
WM contains logic errors, critical flight
information could be unavailable to
the flight crew.
Ultimately, 563 properties about
the WM were developed and checked,
and 98 errors were found and corrected in early versions of the WM model.
This verification was done early in the
design process while the design was
still changing. By the end of the project, the WM developers were checking the properties after every design
change.
Cer TA FCS Phase I. Our second case
study was sponsored by the U.S. Air
Force Research Laboratory (AFRL) under the Certification Technologies for
Advanced Flight Critical Systems (
CerTA FCS) program in order to compare
the effectiveness of model checking
and testing. 12 In this study, we applied
our tools to the Operational Flight
Program (OFP) of an unmanned aerial
vehicle developed by Lockheed Martin Aerospace. The OFP is an adaptive
flight control system that modifies its
behavior in response to flight conditions. Phase I of the project concentrated on applying our tools to the
Redundancy Management (RM) log-
