Qualification of Formal Methods Tools

Presented as part of the 2015 HCSS conference.

Abstract:

Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems such as avionics systems. The recent release of DO-178C and the accompanying Formal Methods supplement DO-333 will make it easier for developers of software for commercial aircraft to obtain certification credit for the use of formal methods.

However, there are still many issues that must be addressed before formal verification tools can be injected into the design process for safety-critical systems. For example, most developers of avionics systems are unfamiliar with which formal methods tools are most appropriate for different problem domains. Different levels of expertise are necessary to use these tools effectively and correctly. Evidence must be provided of a formal method's soundness, a concept that is not well understood by most practicing engineers. Finally, DO-178C requires that a tool used to meet its objectives must be qualified in accordance with the tool qualification document DO-330.

The qualification of formal verification tools will likely pose unique challenges. To address these challenges, we have organized a Dagstuhl seminar (held the week before HCSS). The seminar will include sharing of knowledge from certification experts and formal methods researchers so that each can better understand the challenges and barriers to the use of formal methods tools.

Qualification is not a widely understood concept outside of those industries requiring certification for high-assurance. This presentation will provide background on tool qualification as it impacts the use of formal methods tools for aircraft certification, and include a "hot off the presses" report on results from the Dagstuhl seminar.

Biography:

Darren Cofer is a Fellow in the Rockwell Collins Advanced Technology Center. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His principal area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity avionics systems. His background includes work with formal methods for system and software analysis, the design of real-time embedded systems for safety-critical applications, and the development of nuclear propulsion systems in the U.S. Navy. He has served as the principal investigator on numerous sponsored research projects for NASA, AFRL, and DARPA.