Temporal Verification of Reactive Systems: Safety, Band 2
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.
Invariance Proof Methods
12 In variance Rule
The BottomUp Approach
The TopDown Approach
15 Refining Invariants
41 Invariance Rule for Past Formulas
42 Applications of the Past Invariance Rule
43 Compositional Verification
44 Causality Rule
45 Backward Analysis
46 OrderPreservation Properties
47 History Variables
48 Backto Rule
21 Parameterized Programs
22 SingleResource Allocation
23 MultipleResource Allocation
24 Constructing Linear Invariants
26 FiniteState Algorithmic Verification
32 Nested Waitingfor Rule
33 Verification Diagrams
34 Overtaking Analysis for a Resource Allocator
36 FiniteState Algorithmic Verification
410 FiniteState Algorithmic Verification
Algorithmic Verification of General Formulas
51 Satisfiability of a Temporal Formula
52 Satisfiability over a FiniteState Program
54 Incremental Tableau Construction
55 Particle Tableaux
Andere Ausgaben - Alle anzeigen
additional algorithm appearing applied approach array assertion assume atom await boolean called channel Chapter claim communication completeness computation conclude conjunction connected Consequently consider consists construction contains corresponding cover critical defined definition denote diagram equivalent establish example execution exists expressed fair given graph holds implies incremental inductive infinite initial integer introduced invariant labeled language leads loop forever mutual exclusion node Note observe obtain Obviously operators P-state P-valid particle past formula path position possible preceding premises presented presented in Fig Problem produced proof prove rank reader refer represents request requirement resource rule safety satisfies sequence single solution specified statement step successor synchronous tableau temporal logic termination transition transition relation valid variables verification condition WAIT waiting-for
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...
Logic in Computer Science: Modelling and Reasoning about Systems
Michael Huth,Mark Ryan
Keine Leseprobe verfügbar - 2004
Alle Ergebnisse von Google Books »
Tools and Algorithms for the Construction and Analysis of Systems ..., Band 7
Keine Leseprobe verfügbar - 2001