Abstract: Model-based development, in which models of system behavior are created early in the development process, simulated, then used to automatically generate code and test cases, is becoming increasingly common in the development of avionics software. At the same time, formal verification tools such as model-checkers are rapidly growing more powerful. The convergence of these two trends opens the door for the practical application of formal verification techniques early in the life-cycle for important classes of systems. This talk will describe how Rockwell Collins has applied formal verification tools developed under NASA's Aviation Safety Program to commercial avionics systems in order to reduce costs and improve quality by detecting requirements and design errors early in the lifecycle.

Dr. Steven P. Miller is a Principal Software Engineer in the Advanced Technology Center of Rockwell Collins. He received his Ph.D. in computer science from the University of Iowa in 1991, as well as a B.A. in physics and mathematics in 1974, and has almost 30 years of experience in software development and verification. His current research interests include model-based development, formal methods, and software testing. He was principle investigator on a 5-year project sponsored by NASA Langley's Aviation Safety Program and Rockwell Collins Inc to investigate advanced methods and tools for the development flight critical systems. Prior to that he lead several research efforts at Rockwell Collins, including a collaborative effort with SRI International and NASA to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification system. Appointments: dcm@cs.cmu.edu