Abstract

Aircraft safety has improved steadily over the last few decades and much of this improvement can be attributed to the introduction of advanced automation in the cockpit. However, as these systems grow in complexity and become more tightly integrated, it becomes increasingly difficult for engineers and pilots to anticipate all the ways they may interact. To build the systems of the future, we need to develop methods and tools that will give the engineers the means to analyze their systems while at the same time involving pilots and experts in human-factors.
Rockwell Collins and the NASA Langley Research Center are jointly sponsoring a project for the development of methods and tools for Flight Critical Systems design. This project emphasizes the construction of formal, executable models of system and subsystem requirements. Since these models are executable, they can be connected to mock-ups of the flight deck for validation by pilots and experts in human factors. Since the models are formal, they can be analyzed by theorem provers and model checkers for safety properties.
This talk will provide an overview of the project, demonstrate the simulated execution of the mode logic of a Flight Control System, and show how formal verification is being used to verify safety properties and identify potential sources of pilot mode confusion.

Dr. Steve Miller is a Senior Principal Engineer in the Advanced Technology Center of Rockwell Collins and has over 20 years of experience in software development. He received his Ph.D. in computer science from the University of Iowa in 1991 and a B.A. in physics and mathematics from the University of Iowa in 1974.
His current research interests include requirements modeling and analysis, formal methods, software safety analysis, product family engineering, and software testing. He is principle investigator on a project sponsored by NASA Langley and Collins to investigate advanced methods and tools for the development flight critical systems. Prior to this he lead several research efforts at Collins, including a collaborative effort with SRI International and NASA Langley to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification system.