Theory Matters Wiki

Summary | Rationale | Images | Credits | Powerpoint | Comments | All Nuggets

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

Image:

Attach:LifeCriticalSystems.jpg

Comments

• to give feedback on this nugget, just add another bullet to this list
• I wonder if the first two sentences of the rationale can be added to the summary. The term "formal methods" appears in the summary without explanation. I think it is important to make the summary self-contained and understandable without reading further. The point is the term "formal methods" has a specific meaning in computer science, but the words are common enough that folks reading the summary might have their own idea of what it is. Richard L.
  • KYR: Good point. I like the sentences in the summary to create the sense of urgency but I tried to make it clearer what I was talking about.
• I like the last sentence that cites the importance of formal methods, but it would be stronger if there were some listed applications. Already mentioned are flying, nuclear power plants, and medical devices. What else. I might add automobiles, trains, anything to do with high speed transportation. - Richard L.
  • KYR: Also financial systems and security. Intel uses them to verify CPU's too... I'm unclear as to where you want me to mention other life-critical systems, though. I lead in with the most common ones and then tried to branch out to the theoretical description from there.
• This may be another nugget, but I wonder if there is a way to tie in the human in the loop (as Jeannette Wing likes to say). Can formal methods include humans and computers in safety critical processes? Richard L.
  • KYR: That is definitely a whole different nugget.
• The current rationale seems to have a "breadth" theme, giving a summary of the many different aspects of formal methods research, without directly connecting them to the "Life-Critical" theme of the nugget. An alternative approach would be to use the Rationale for "depth", elaborating and focusing on research themes and challenges needed for formal methods to extend its utility for Life-Critical System Verification. - Salil
  • KYR: Yes -- I definitely went for the breadth theme. There are so many popular verification techniques and I wanted to make sure to at least explicitly mention the names of the most widely-used ones so that it's abundantly clear what research areas I'm talking about. I think it's really important to do that. I chose this way because I think the depth approach would necessitate a significantly longer rationale than you were looking for. Also, I think understanding the challenges for FM research first requires a knowledge of the techniques we're using currently and then a familiarity with their limitations. For example, one of the biggest challenges is the state space explosion problem, which is not understandable unless you're familiar with the way a model checker works internally. Since formal methods are not covered at all in most undergraduate CS programs and we were directed to write the rationale assuming no more than a BS in CS, I also figured the deeper material might be inappropriate for the intended audience.
• Minor suggestions - Salil
  • I wonder if "mathematical logic" would be better than "logic and mathematics" in the tagline (not sure).
    • KYR: I think that while "mathematical logic" flows a bit better, "logic and mathematics" may be a better general description, especially for this audience.
  • start new par after "high level of assurance"
    • KYR: I thought the summary was supposed to be only one paragraph?
    • SV: That guideline was more to give an indication of length rather than a strict rule about format. My suggestion to start a new par was mainly so that the positive contribution of TCS is more prominent.
    • KYR: OK. done.
  • "...testing but the significantly higher level of...outweighs" -> "testing. But they provide a significantly higher level of assurance that outweighs..." [current sentence is a bit long and hard to parse]
    • KYR: done.
  • put first occurrences of "model checking", "automated theorem proving", "fault-tolerant designs", "Model-based development" in italics (if the goal is to help the reader identify these subfields of formal methods)
    • KYR: done.
  • "systems which can" -> "systems that can"
    • KYR: done.
• Note from designer Elaine Park: Just added the extra text and resized the image for Powerpoint proportions. I threw a darker background in since readability becomes an issue with the added tagline.