9783540415237

Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct.This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available.

Part I. Principles and Techniques

Introduction

3

(2)

Automata

5

(22)

Introductory Examples

5

(4)

A Few Definitions

9

(2)

A Printer Manager

11

(1)

A Few More Variables

12

(2)

Synchronized Product

14

(7)

Synchronization by Message Passing

21

(3)

Synchronization by Shared Variables

24

(3)

Temporal Logic

27

(12)

The Language of Temporal Logic

28

(4)

The Formal Syntax of Temporal Logic

32

(1)

The Semantics of Temporal Logic

33

(2)

PLTL and CTL: Two Temporal Logics

35

(2)

The Expressivity of CTL

37

(2)

Model Checking

39

(8)

Model Checking CTL

39

(3)

Model Checking PLTL

42

(3)

The State Explosion Problem

45

(2)

Symbolic Model Checking

47

(12)

Symbolic Computation of State Sets

47

(4)

Binary Decision Diagrams (BDD)

51

(3)

Representing Automata by BDDs

54

(2)

BDD-based Model Checking

56

(3)

Timed Automata

59

(20)

Description of a Timed Automaton

60

(2)

Networks of Timed Automata and Synchronization

62

(2)

Variants and Extensions of the Basic Model

64

(3)

Timed Temporal Logic

67

(1)

Timed Model Checking

68

(11)

Conclusion

73

(4)

Part II. Specifying with Temporal Logic

Introduction

77

(2)

Reachability Properties

79

(4)

Reachability in Temporal Logic

79

(1)

Model Checkers and Reachability

80

(1)

Computation of the Reachability Graph

80

(3)

Safety Properties

83

(8)

Safety Properties in Temporal Logic

83

(1)

A Formal Definition

84

(2)

Safety Properties in Practice

86

(1)

The History Variables Method

87

(4)

Liveness Properties

91

(8)

Simple Liveness in Temporal Logic

92

(1)

Are Liveness Properties Useful?

92

(2)

Liveness in the Model, Liveness in the Properties

94

(2)

Verification under Liveness Hypotheses

96

(1)

Bounded Liveness

97

(2)

Deadlock-freeness

99

(4)

Safety? Liveness?

99

(1)

Deadlock-freeness for a Given Automaton

99

(2)

Beware of Abstractions!

101

(2)

Fairness Properties

103

(6)

Fairness in Temporal Logic

103

(1)

Fairness and Nondeterminism

104

(1)

Fairness Properties and Fairness Hypotheses

104

(2)

Strong Fairness and Weak Fairness

106

(1)

Fairness in the Model or in the Property?

107

(2)

Abstraction Methods

109

(22)

When Is Model Abstraction Required?

110

(1)

Abstraction by State Merging

110

(1)

What Can Be Proved in the Abstract Automaton?

110

(4)

Abstraction on the Variables

114

(4)

Abstraction by Restriction

118

(2)

Observer Automata

120

(11)

Conclusion

125

(4)

Part III. Some Tools

Introduction

129

(2)

SMV -- Symbolic Model Checking

131

(8)

What Can We Do with SMV?

131

(1)

SMV's Essentials

131

(1)

Describing Automata

132

(3)

Verification

135

(1)

Synchronizing Automata

136

(1)

Documentation and Case Studies

137

(2)

SMV Bibliography

138

(1)

SPIN -- Communicating Automata

139

(6)

What Can We Do with Spin?

139

(1)

Spin's Essentials

139

(1)

Describing Processes

140

(1)

Simulating the System

141

(1)

Verification

142

(2)

Documentation and Case Studies

144

(1)

Spin Bibliography

144

(1)

DESIGN/CPN -- Coloured Petri Nets

145

(8)

What Can We Do with Design/CPN?

145

(1)

Design/CPN's Essentials

145

(1)

Editing with Design/CPN

146

(1)

Simulating the Net

147

(2)

Analyzing the Net

149

(1)

Documentation and Case Studies

149

(4)

Design/CPN Bibliography

150

(3)

UPPAAL -- Timed Systems

153

(8)

What Can We Do with Uppaal?

153

(1)

UPPAAL's Essentials

153

(1)

Modeling Timed Systems with Uppaal

154

(3)

Simulating a System

157

(1)

Verification

157

(1)

Documentation and Case Studies

158

(3)

UPPAAL Bibliography

158

(3)

KRONOS -- Model Checking of Real-time Systems

161

(8)

What Can We Do with Kronos?

161

(1)

KRONOS' Essentials

161

(1)

Describing Automata

162

(2)

Synchronized Product

164

(1)

Model Checking

165

(2)

Documentation and Case Studies

167

(2)

KRONOS Bibliography

167

(2)

HYTECH -- Linear Hybrid Systems

169

(10)

What Can We Do With HyTech?

169

(1)

HyTech's Essentials

169

(1)

Describing Automata

170

(2)

System Analysis

172

(2)

Parametric Analysis

174

(2)

Documentation and Case Studies

176

(3)

HYTECH Bibliography

176

(3)

Main Bibliography

179

(4)

Index

183

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

Amazon no longer offers textbook rentals. We do!

Amazon no longer offers textbook rentals. We do!

We're the #1 textbook rental company. Let us show you why.

Systems and Software Verification

3540415238

Supplemental Materials

Summary

Table of Contents

Supplemental Materials

Rewards Program