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
array assume at-m auxiliary variables await boolean channel chopstick claim computation concurrent programs Consider program construction contains critical section defined Dekker's algorithm denote dining philosophers problem E.M. Clarke equivalent establish even(y expressed fair transition system fulfilling given holds at position implies incremental inductive assertion infinite integer integer square root INV-B labeled loop forever message passing minimal rank module mutual exclusion nested waiting-for formula node noncritical obtain overtaking P-accessible P-invariant P-state valid P-valid particle past formula path Peterson's algorithm Pnueli presented in Fig process PI program MUX-PETI program MUX-SEM program PROD-CONS proof prove r-successor reachable reader is requested readers-writers problem refer requirement resource rule INV rule INV-P safety property satisfies semaphores sequence solution specified subformula subgraph successor synchronous system variables temporal formula temporal logic termination transition relation verification condition virtual variables
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
Tiziana Margaria,Wang Yi
Keine Leseprobe verfügbar - 2001