| All Nuggets

Summary | Rationale | Powerpoint | JPG Slide | JPG Image | Credits | Comments

• 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.

Summary | Rationale | Images | Credits | Powerpoint | Comments

• KYR: OK. done.

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.

• 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.

• SV: That was more to give an indication of length rather than a strict rule about format. The suggestion was mainly so that the positive contribution of TCS is more prominent.

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.

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.

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.

• 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.

• 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.

• KYR: That is definitely a whole different nugget.

• 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.

• KYR: I think that while "mathematical logic" flows a bit better, "logic and mathematics" may be a better general description, especially for this audience.

• KYR: I thought the summary was supposed to be only one paragraph?

• KYR: done.

• KYR: done.

• KYR: done.

• 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.
• 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
• Minor suggestions - Salil
  • I wonder if "mathematical logic" would be better than "logic and mathematics" in the tagline (not sure).
  • start new par after "high level of assurance"
  • "...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]
  • 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)
  • "systems which can" -> "systems that can"

• 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.
• 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.
• 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.

• 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.

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 formal methods research for the verification of ever more challenging problem domains.

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 \emph{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 which 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.

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 but the significantly higher level of assurance provided by formal verification 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, automata theory, temporal logics, and graph theory.

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, automata theory, temporal logics, and graph theory.

[Explanation of theorem proving]

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 timeframes. 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 formal methods research for the verification of ever more challenging problem domains.

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 cost up front than simulations or other forms of testing but the significantly higher level of assurance provided by formal verification 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. [Explanation of model checking][Explanation of theorem proving]

[Conclusion and mention of other formal methods.]

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

Attach:LifeCriticalSystems.jpg

Salil Vadhan; image designed by Raymond V. Meyer

Image:

this Δ.

Cynthia Dwork, Kristin Yvonne Rozier, Amit Sahai, Salil Vadhan,

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

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 algorithms in reasonable timeframes. 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 formal methods research for the verification of ever more challenging problem domains.

Cynthia Dwork Kristin Yvonne Rozier Amit Sahai Salil Vadhan ... picture credit coming soon...

Image is under development and will be uploaded soon. (You can also upload images you've find using a command like this Δ.)

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

Life-Critical System Verification

Put the tagline here.

Summary

Put the summary here. It should be brief (eg 200 words) and accessible to a general audience.

Rationale

Put a slightly more detailed explanation here, which can be aimed at a general computer scientists.

Contributors and Credits

List people who have worked on this nugget and any sources of text, images, etc.

Image Ideas

List ideas for possible images. You can also upload images you've find using a command like this Δ.

Comments

• to give feedback on this nugget, just add another bullet to this list