Skip to main content
main-content

Über dieses Buch

This book is about the verification of reactive systems. A reactive system is a system that maintains an ongoing interaction with its environment, as opposed to computing some final value on termination. The family of reactive systems includes many classes of programs whose correct and reliable construction is con­ sidered to be particularly challenging, including concurrent programs, embedded and process control programs, and operating systems. Typical examples of such systems are an air traffic control system, programs controlling mechanical devices such as a train, or perpetually ongoing processes such as a nuclear reactor. With the expanding use of computers in safety-critical areas, where failure is potentially disastrous, correctness is crucial. This has led to the introduction of formal verification techniques, which give both users and designers of software and hardware systems greater confidence that the systems they build meet the desired specifications. Framework The approach promoted in this book is based on the use of temporal logic for specifying properties of reactive systems, and develops an extensive verification methodology for proving that a system meets its temporal specification. Reactive programs must be specified in terms of their ongoing behavior, and temporal logic provides an expressive and natural language for specifying this behavior. Our framework for specifying and verifying temporal properties of reactive systems is based on the following four components: 1. A computational model to describe the behavior of reactive systems. The model adopted in this book is that of a Fair Transition System (FTS).

Inhaltsverzeichnis

Frontmatter

Chapter 0. Preliminary Concepts

Abstract
This book presents methods for verifying that reactive programs satisfy their specifications, where the specifications are formulated in temporal logic.
Zohar Manna, Amir Pnueli

Chapter 1. Invariance: Proof Methods

Abstract
According to the classification of properties, a safety property is a property that can be specified by a formula of the form □ p for a past formula p.
Zohar Manna, Amir Pnueli

Chapter 2. Invariance: Applications

Abstract
Chapter 1 introduced the main method for proving that an assertion p is an invariant of program P. This method is essentially an induction on the positions in the computation. In this chapter we also identified the creative step of finding an inductive assertion that strengthens a given candidate invariant as the most difficult task in proofs of invariance. Some heuristics, such as supplementing assertions by preconditions, were proposed as techniques that may aid in the construction of inductive assertions.
Zohar Manna, Amir Pnueli

Chapter 3. Precedence

Abstract
In this chapter we present methods for verifying safety properties that are expressed by nested waiting-for (nested unless) formulas of the general form
$$ p\,\, \Rightarrow \,\,{q_m}\,w\,\,{q_{m - 1}}\,\, \ldots \,\,{q_1}\,w\,{q_0},$$
for state formulas (assertions) p,q0,q,1,…,q m . Recall (see page 48) that a computation satisfies this formula if every p-position starts a succession of intervals, that can be summarized by the following figure:
https://static-content.springer.com/image/chp%3A10.1007%2F978-1-4612-4222-2_4/MediaObjects/978-1-4612-4222-2_4_Fig1_HTML.jpg
Each q i -interval, 1 ≤ im, is a set of successive positions which all satisfy q i and may be empty or extend to infinity.
Zohar Manna, Amir Pnueli

Chapter 4. General Safety

Abstract
We have defined a safety property to be any property that can be specified by a formula of the form □ p for some past formula p.
Zohar Manna, Amir Pnueli

Chapter 5. Algorithmic Verification of General Formulas

Abstract
At the end of each of Chapters 2–4, we presented an algorithm for checking whether a property belonging to the class of properties considered in that chapter is valid over a given finite-state system.
Zohar Manna, Amir Pnueli

Backmatter

Weitere Informationen