Temporal Verification of Reactive Systems: Safety, Band 2

Cover
Springer Science & Business Media, 04.08.1995 - 512 Seiten
0 Rezensionen
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
447
55 Particle Tableaux
455
Problems
464
Bibliographic Remarks
466
References
469
Index to Symbols
485
General Index
493
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 471 - Bryant, RE (1986). Graph-based algorithms for Boolean function manipulation. IEEE Trans.
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 472 - 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...

Verweise auf dieses Buch

Alle Ergebnisse von Google Books &raquo;

Über den Autor (1995)

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

Bibliografische Informationen