ADGS-2100 Display Window Manager Analysis

Commercial Displays Model-Checking (Powerpoint Talk)

As part of the Methods and Tools project, Rockwell Collins applied the formal verification technology developed on the project to the window manager of the ADGS-2100 Adaptive Display and Guidance System. The window manager ensures that data from different displays applications is routed to the correct display, and that critical applications are displayed even in the event of display or computing resource failures. It is specified as Simulink model with more than 16,000 Simulink primitive Simulink blocks organized into over 4,000 Simulink subsystem instances.

The majority of the functional behavior of the window manager was verified against the high-level requirements expressed as 563 temporal logic properties. During this effort, 98 errors in the high-level requirements and Simulink models were found and corrected. This provides an industrial example of how formal methods can be easily and cost-efficiently introduced to remove defects early in the design cycle.

Publications on the ADGS-2100 Display Window Manager Analysis

• Michael W. Whalen, John D. Innis, Steven P. Miller, and Lucas G. Wagner, ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis, NASA Contractor Report, November 2005.