Life-Critical System Verification

 

 

“If it fails, people die.” Theoretical computer scientists harness the power of logic and mathematics to provide a provable guarantee of safety.

Summary

Life-critical systems have become ubiquitous in our everyday lives and grow increasingly complex every year. They fly our planes, control our nuclear power plants, run our medical devices, and so much more. Yet, how do we know they are safe? Verification techniques such as exhaustive testing and simulation could take millions of years, or longer, to certify a system to a high level of assurance.

Theoretical computer scientists have developed a successful paradigm for life-critical system verification. Systems can and should be designed from the start to enable automated verification. Then we can use formal methods to analyze life-critical systems and provide absolute assurances of software or hardware safety in reasonable time-frames. Recent algorithmic advances have vastly increased the size and complexity of the systems which we can analyze using formal verification methods. However, today’s verification techniques do not scale with the ever-increasing complexity and diversity of modern life-critical systems. There is an urgent need to extend research in formal methods for life-critical system verification to handle ever more challenging problem domains.

Rationale

Computer scientists use formal methods for the design, specification, and verification of life-critical hardware and software systems. Formal methods refers to a collection of verification techniques, all of which entail the utilization of mathematical logic to provide checks of correctness with a very high level of assurance. Currently, using formal methods for verification requires significantly more time and higher cost up front than simulations or other forms of testing. However, they provide a significantly higher level of assurance that outweighs the initial cost of implementation in the case of systems where human life or security is at risk. To achieve the equivalent assurance of correctness, simulations would have to be run for unachievable periods of time. Formal methods have been successfully used to verify systems such as air traffic control, airplane separation assurance, autopilot, CPU designs, life-support systems, medical equipment, such as devices which administer radiation, and many other systems which ensure human safety.

Two of the most popular formal methods for verification are model checking and automated theorem proving. Model checking involves creating a formal model of the system to be verified. Usually this is done in one of several popular modeling languages. A formal specification of the safety property to be verified is written in temporal logic. The specification is then negated and combined with the system model. Finally, an exhaustive search of the state space reveals whether or not there is a path through this combined system model from a start state to some accepting condition. If there is such a path, the system does not always uphold the safety property. The path is then called a counterexample trace and it provides a sequence of steps which leads to the erroneous unsafe behavior. If there is no such path, then the system model always satisfies the safety property specification. Research topics within model checking include Binary Decision Diagrams (BDDs), satisfiability (SAT), Satisfiability Modulo Theory (SMT), automata theory, temporal logics, and graph theory.

Like model checking, automated theorem proving requires the system to be described in a formal, though not necessarily executable, language. Specifying systems in an automated theorem prover aids in system design by requiring the programmer to describe the system behavior in a very logical way and then satisfy type-checks and other proof obligations. Safety properties are introduced as theorems which must be proven to hold given the formal description of the system behavior, a set of logical axioms, and a set of inference rules. While some proofs can be completed fully automatically, most require a programmer to guide the automated theorem prover through the proof steps. Each step is checked by the theorem prover to ensure the programmer does not make illogical leaps during the proof. If the safety property does not hold, the programmer will encounter a proof step which cannot be discharged and which describes the circumstances of the bug. Research topics within automated theorem proving include decision procedures, automated deduction, operational semantics, non-linear arithmetic, constraint solving, quantified boolean formulas, term rewriting, and answer set programming.

Formal methods can be successfully used for ensuring the reliability of software and hardware at all stages of design and development. Fault-tolerant designs allow for the creation of systems that can continue functioning properly after encountering errors. Model-based development facilitates the detection of bugs before system implementation. Systems can then be implemented from verified models. Code annotation systems and translators which produce proofs directly from code allow verification during the software development phase. Theoretical tools such as hybrid automata and separation logic allow for reasoning about complex system interactions. There are many promising tools and techniques which comprise formal methods for the verification of life-critical systems. Investing in their development and implementation is the best way to ensure that the systems which hold our lives in their hands everyday are safe.

Contributors and Credits

Cynthia Dwork, Kristin Yvonne Rozier, Amit Sahai, Salil Vadhan; image designed by Raymond V. Meyer

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: