Temporal Verification of Reactive Systems: Safety, Band 2

Cover
Springer Science & Business Media, 04.08.1995 - 512 Seiten
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).
 

Was andere dazu sagen - Rezension schreiben

Es wurden keine Rezensionen gefunden.

Inhalt

Invariance Proof Methods
81
12 In variance Rule
87
The BottomUp Approach
104
The TopDown Approach
111
15 Refining Invariants
127
Problems
152
Bibliographic Remarks
164
Invariance Applications
167
41 Invariance Rule for Past Formulas
318
42 Applications of the Past Invariance Rule
327
43 Compositional Verification
336
44 Causality Rule
342
45 Backward Analysis
347
46 OrderPreservation Properties
354
47 History Variables
357
48 Backto Rule
363

21 Parameterized Programs
168
22 SingleResource Allocation
179
23 MultipleResource Allocation
191
24 Constructing Linear Invariants
201
25 Completeness
220
26 FiniteState Algorithmic Verification
227
Problems
232
Bibliographic Remarks
248
Precedence
251
32 Nested Waitingfor Rule
264
33 Verification Diagrams
272
34 Overtaking Analysis for a Resource Allocator
280
35 Completeness
288
36 FiniteState Algorithmic Verification
297
Problems
307
Bibliographic Remarks
314
General Safety
317
49 Completeness
372
410 FiniteState Algorithmic Verification
381
Problems
392
Bibliographic Remarks
396
Algorithmic Verification of General Formulas
399
51 Satisfiability of a Temporal Formula
400
52 Satisfiability over a FiniteState Program
422
Examples
434
54 Incremental Tableau Construction
443
55 Particle Tableaux
451
Problems
460
Bibliographic Remarks
462
References
465
Index to Symbols
481
General Index
489
Urheberrecht

Andere Ausgaben - Alle anzeigen

Häufige Begriffe und Wortgruppen

Beliebte Passagen

Seite 2 - This is an assertion characterizing all the initial states, ie, states at which the computation of the program can start. A state is defined to be initial if it satisfies 6. We define the state s...
Seite 2 - A finite set of state variables. Some of these variables represent data variables, which are explicitly manipulated by the program text. Other variables are control variables, which represent, for example, the location of control in each of the processes in a concurrent program. We assume each variable to be associated with a domain, over which it ranges.
Seite 5 - For the case that fc = 1, we write simply u := e. • Await: For a boolean expression c, await c is an await statement. We refer to condition c as the guard of the statement. Execution of await c changes no data variables.
Seite 4 - T, it is not the case that r is continually enabled beyond some position j in a (ie, r is enabled at every position k > j) while r is not taken beyond j.
Seite 50 - In the sequel, we adopt the convention by which a formula p that is claimed to be valid is state valid if p is an assertion, and is temporally valid if p contains at least one temporal operator. Two formulas p and q are defined to be equivalent, denoted p ~ q, if the formula p «-> q is valid, ie, a E p iff at= q, for all models a.
Seite 468 - P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program.
Seite 3 - ' is a r-successor of s} We say that the transition T is enabled on the state s, if T(S) ^ <j>. Otherwise, we say that T is disabled on s. We say that a state s is terminal if all the transitions T £ T are disabled on it.
Seite 57 - P-valid. 2.5 Specification of Properties A temporal formula ^ that is valid over a program P specifies a property of P, ie, states a condition that is satisfied by all computations of P. The properties expressible by temporal logic can be arranged in a hierarchy that identifies different classes of properties according to the form of formulas expressing them. Here we will consider only properties falling into the two most important classes: safety and response. Safety...

Über den Autor (1995)

Amir Pnueli is Professor of Computer Science at the Weizmann Institute of Science in Israel.

Bibliografische Informationen