Lessons from Twenty Years of Industrial Formal Methods

Presented as part of the 2012 HCSS conference.

Abstract:

Over the last two decades formal methods have achieved widespread use by industry in the development of safety and security critical systems. However, these successes often go unacknowledged as evidence of the successful transition of formal methods simply because

the name “formal methods” is often still associated with its early prototypes rather than with the successful methods and tools they have evolved into. To better understand the benefits that formal methods can provide, Rockwell Collins has conducted many experiments over the last

twenty years in their use. This paper describes several of these experiments, discusses what worked and what didn’t, and identifies the key lessons we have learned about introducing formal methods into an industrial setting.

Biography:

Steven Miller is a Principal Software Engineer in the Advanced Technology Center of Rockwell Collins with over 30 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 research interests include formal methods, model-based development, requirements modeling and analysis, and software testing. He was the principal investigator on a five year project sponsored by NASA Langley and Rockwell Collins to develop advanced methods and tools for the development flight critical systems. Other projects he has led include an Air Force Research Labs project to apply formal verification to adaptive flight control systems and a collaborative effort with SRI International and NASA Langley to formally verify the microcode in the AAMP5 and AAMP-FV microprocessors.