Computer Science

Colloquium Details

Provable Safety for High-Consequence Systems

Abstract

Increasingly, digital systems are being deployed in high-consequence applications. In these domains, such as transportation and defense, "bugs" may cost lives. Functional testing is insufficient to ensure the safety of such systems because it exercises only a tiny fraction of the system's digital behavior. Formal methods offer much stronger safety guarantees, but existing tools are intractable for complex specifications. We have developed a tractable approach to formally-verified design based on the theory of refinement. With this method, an abstraction of the desired system is first proven to meet some specification. Then, details are added gradually with proof of correctness ensured at each step, until an executable program has been derived. Our current work seeks to prove the effectiveness of this approach for high-consequence systems, based on an implementation in the Coq theorem prover. In this talk I will give an overview of the theory, the challenges of applying it in practice, and describe the results of our ongoing implementation effort.

Biography

Geoff Hulette works in the Scalable and Secure Systems Research group at Sandia National Laboratories, specializing in digital design for critical systems. His research focuses on applying techniques from programming language theory and formal verification to the problem of designing high-consequence digital and hybrid digital/analog systems that are "correct by construction." He has a Ph.D in Computer Science from the University of Oregon.