√лавна€    Ex Libris     ниги    ∆урналы    —татьи    —ерии     аталог    Wanted    «агрузка    ’удЋит    —правка    ѕоиск по индексам    ѕоиск    ‘орум   

ѕоиск по указател€м

Clarke E.M., Grumberg O., Peled D.A. Ч Model checking
Clarke E.M., Grumberg O., Peled D.A. Ч Model checking

ќбсудите книгу на научном форуме

Ќашли опечатку?
¬ыделите ее мышкой и нажмите Ctrl+Enter

Ќазвание: Model checking

јвторы: Clarke E.M., Grumberg O., Peled D.A.


Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1998 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers.
The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years.
This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers.

язык: en

–убрика: “ехнологи€/

—татус предметного указател€: √отов указатель с номерами страниц

ed2k: ed2k stats

√од издани€: 2000

 оличество страниц: 314

ƒобавлена в каталог: 04.12.2005

ќперации: ѕоложить на полку | —копировать ссылку дл€ форума | —копировать ID
ѕредметный указатель
$\mu$-calculus      69 97Ч108
$\mu$-calculus, complexity      101 103 108
$\mu$-calculus, CTL translated into      107Ч108
$\mu$-calculus, OBDDs      104Ч107
Abstractions      193Ч213
Abstractions, approximations, computing      199Ч202
Abstractions, approximations, exact      202Ч203
Abstractions, automation      293Ч294
Abstractions, data abstraction      195Ч213
Abstractions, examples      204Ч213
Abstractions, future research on      293Ч294
Abstractions, infinite families      242Ч248
Abstractions, introduction to      10
Abstractions, symbolic      210Ч213
Abstractions, usefulness of      195Ч196
Accepting, in automata theory      121Ч122
Action transitions      268
ACTL      31 32
ACTL*      31 32
ACTL*, abstractions      197 202
ACTL*, simulation      177 232
ACTL, abstractions      196
ACTL, bisimulation      178
ACTL, compositional reasoning      186Ч191
ACTL, tableau construction      180Ч184 186
Aircraft controller example      259Ч264
Alternation depth      97 100 108
ALU example      75Ч77 85Ч87
Always operator      27
Ample sets      9 143Ч154
Ample sets, calculation of      144 154Ч160
Ample sets, selection of      147Ч151 154Ч155
Apply algorithm      56Ч57
assignment statement      21
Assume-guarantee reasoning      10 181 185Ч186 189Ч190 see
Asynchronous execution      17
asynchronous systems      8 19Ч20
atom      43
Atomic transitions      16
Automata theory      121Ч140
Automata theory, advantages of      123
Automata theory, deterministic automata      127Ч128
Automata theory, emptiness checking      129Ч132
Automata theory, finite and infinite words      121Ч122
Automata theory, generalized automata      128Ч129
Automata theory, infinite families      245Ч248
Automata theory, intersection and complementation      124Ч127
Automata theory, language containment checking      139Ч140
Automata theory, LTL      125 132Ч138
Automata theory, nondeterministic automata      127Ч128
Automata theory, OBDDs      57
Automata theory, on-the-fly model checking      138Ч139
Automata theory, partial order reduction      167Ч168
Automata theory, timed automata      265Ч291
Automatic methods, advantages of      xiЧxii xiii 3
Automorphisms      216Ч221
Binary decision diagrams (BDDs)      52Ч59
Binary decision diagrams, isomorphic      53
Binary decision diagrams, partitioned transition relations      84Ч85
Binary decision diagrams, transformation rules      53
Binary decision diagrams, usefulness of      xiv
Binary decision trees      51Ч52 240 242
Bisimulation      171Ч180
Bisimulation, abstractions      194Ч195 202Ч203
Bisimulation, largest      179Ч180
Bisimulation, quotient models      220
Bitwise operations, and abstraction      208Ч210
BLOCKS      146 226
Boolean attributes      116
boolean formulas      7 see
Bound variables      98
Bounded until operator      255Ч256
Branching structure      5 6 30
Buechi automata      122 123
Buechi automata, emptiness checking      129Ч132
Buechi automata, generalized      128Ч129
Buechi automata, intersection and complementation      124Ч127
Buechi automata, language containment      139Ч140
Buechi automata, LTL      132Ч138
Buechi automata, nondeterministic      127Ч128
Bus architecture      112Ч120 see
Busy waiting statement      24
Cache coherence protocol      7Ч8
Cache coherence protocol, invariants      235Ч238
Cache coherence protocol, SMV      112Ч120 235
Cache coherence protocol, symmetry      228Ч230
Canonical representations      52Ч53 288Ч289
Chinese remainder theorem      206
Clock constraints      266Ч267
Clock regions      274Ч280
Clock reset operation      281 289
Clock zones      280Ч291
clocks      266Ч291
Closed formulas      98
Code regions      109Ч110
Commutativity      141 144Ч145 147
Complementation      124Ч127
Completeness      4 5 6 41 180
Cycle condition      150Ч151 155 159Ч160
Cycles, in group theory      216
Data abstraction      195Ч213
Data abstraction, approximations, computing      199Ч202
Data abstraction, approximations, exact      202Ч203
Data abstraction, examples      204Ч213
Data abstraction, pushing inward      200Ч202
Deductive verification      2Ч3 see
Delay transitions      267
Dependability metrics      295
Dependency relation      141 144Ч145 157
Depth first search (DFS)      129Ч132 139
Depth first search, partial order reduction      143 147Ч154 160 168
Design validation, problem of      see "Model checking"
Deterministic automata      127Ч128
Deterministic structures      179 180
Deterministic transitions      109 141
DFS      see "Depth first search"
Difference bound matrices      283 287Ч291
digital circuits      17Ч20
Directed acyclic graph      52
Disabled transitions      141
Discrete real-time systems      254 255Ч264 265
Disjunctive partitioning      79 80
Domain of Interpretation      14
Dynamic reordering      54Ч55
Efficiency, abstractions      197
Efficiency, automata theory      138Ч139
Efficiency, partial order reduction      143
Efficiency, symbolic model checking      80Ч87
Elapsing of time operation      281Ч282 289
embedded systems      2
Emptiness checking, of Buechi automata      129Ч132
Enabled transitions      141 143Ч144 147Ч151 see
Enabledness      144
Entry point, of a statement      20
Equivalences bisimulation      see "Bisimulation"
Equivalences language      179Ч180 232
Equivalences simulation      see "Simulation preorder"
Equivalences stuttering      146Ч154 163Ч164
Error trace      4 see
Eventuality sequence      43
Eventually operator      27
Exhaustive exploration      xi
Exit point, of a statement      20
Explosion      see "State explosion"
Failure, probability of      295
Fair bisimulation relation      175
Fair semantics      32
Fair simulation relation      178 186
Fairness      32Ч33
Fairness constraints      20 32Ч33 40Ч41 59
Fairness constraints, bisimulation      171 175 179 180
Fairness constraints, compositional reasoning      186 187
Fairness constraints, simulation      178 186
Fairness constraints, SMV      111
Fairness constraints, symbolic model checking      68Ч71 72Ч74 91Ч95
Finite automaton      121 see
Finite versus infinite state systems      3
Finite words      121Ч122 see
Fixpoints      61Ч66
Fixpoints, $\mu$-calculus      97Ч108
Fixpoints, fairness constraints      69Ч70
Fixpoints, future research on      293
Fixpoints, introduction to      7
Flagged node      130
Floyd Ч Warshall Algorithm      288
Formal verification, need for      1Ч2 see
Free variables      98
Full symmetric groups      215 226 228
Fully expanded state      147
Futurebus+ standard      7Ч8
Futurebus+ standard, invariants      235Ч238
Futurebus+ standard, SMV      112Ч120 235
Futurebus+ standard, symmetry      228Ч230
Globally operator      27
Grammars, future research on      294Ч295
Grammars, infinite families and      238Ч248
Granularity      16Ч17
Graph grammars      238Ч239
Graph isomorphism problem      224Ч225
Graphs, decomposition into SCCs      36 44
Graphs, encoding techniques      293
Graphs, region      279Ч280 291
Graphs, tableau construction      42 87Ч95
Graphs, zone      283Ч284 289
Greedy algorithm      83 84
Group theory      215Ч221
guard      165 266
Hashed node      130
ICTL* (indexed CTL*)      231
Independence relation      144Ч145
Independent events      9
Induction technique      11
Infinite families      231Ч252
Infinite families, example, Futurebus+      235Ч238
Infinite families, example, token ring      232Ч233 248Ч252
Infinite families, grammars, graph and network      238Ч248
Infinite families, invariants      232Ч238 241Ч242
Infinite families, temporal logic      231Ч232
Infinite families, undecidability      231 248Ч252
Infinite versus finite state systems      3
Infinite words      121Ч122 see
Initial states      14Ч15 27 35
Instantaneous transitions      265
Interleaved composition      109
Interleaved execution      17
Interleaving model      9 19 141 142
Internet      2
Intersection operation, automata theory      124Ч127
Intersection operation, clock zones      281
Intersection operation, difference bound matrices      289
Invariance groups      219Ч221
Invariant processes      11
Invariant rule      233 241
Invariants, clock constraints      266
Invariants, infinite families      232Ч238 241Ч242
Invisibility      145 147 149Ч150
Kripke structures      13
Kripke structures, $\mu$-calculus modification      98
Kripke structures, abstractions      196Ч197 199Ч200 204
Kripke structures, automata theory      123
Kripke structures, automorphism group      216Ч221
Kripke structures, CTL* semantics      29
Kripke structures, definition      14
Kripke structures, example      26
Kripke structures, extraction      14Ч17
Kripke structures, fairness      33
Kripke structures, infinite families      231Ч232 238Ч242
Kripke structures, model checking algorithms      35Ч49
Kripke structures, OBDDs and encoding      51 57Ч59
Kripke structures, partial order reduction      141
Kripke structures, symbolic model checking      61Ч95
Labeling transformations      20Ч23
Language, automata theory      121Ч122 139Ч140
Language, equivalence      179Ч180 232
Language, synchronous      203Ч204
Leader election algorithm      165Ч166
Length, of a path      142
Lichtenstein Ч Pnueli algorithm      42 87
Linear structure      5 6 30
Linear Temporal Logic      see "LTL"
Locations, and timed automata      265Ч291
lock statement      24
Logarithms      208
LTL (Linear Temporal Logic)      5 6 30
LTL, automata theory      125 132Ч138
LTL, invariants      232
LTL, model checking algorithm      41Ч46
LTL, partial order reduction      146Ч154 159 164
LTL, symbolic model checking      87Ч95
Maximum delay algorithm      257Ч259
Mean Time Between Failures      295
message exchange      17
Microwave oven example      38Ч39 47Ч49
Minimum delay algorithm      257
Model checking problem      35
Model checking, advantages of      1 3 293
Model checking, compared to other methods      2Ч3
Model checking, future research on      293Ч295
Model checking, limitations of      xiii 1 293
Model checking, need for      xi 1Ч2
Model checking, on-the-fly      138Ч139
Model checking, process of      4
Model checking, using representatives      141 see
Modeling, as step in model checking      4 13Ч26
Modeling, as step in model checking, example      24Ч26
Modeling, as step in model checking, first-order representations      14Ч16
Modeling, as step in model checking, granularity      16Ч17
Modeling, as step in model checking, Kripke structure defined      14
Modeling, as step in model checking, types of concurrent systems      17Ч24
Modular structure      10
Modules, in SMV      109
Monitor task servers      260
Monotonicity of composition      233
Monotonicity, syntactic      98
Moore machine      204
Mutual exclusion      24
Mutual exclusion, SMV      109Ч112
Negation normal form      132
Network grammars      239Ч248 295 see
Never claim construct      167
Next state variables      15
Next time operator      27
nodes      130 133
Noncritical region      25 109 111
Nondeterministic Buechi automata      127Ч128
Nondeterministic structures      179 180
Nondeterministic transitions      109
Nonterminal vertices      51Ч52
OBDDs      see "Ordered binary decision diagrams"
On-the-fly model checking      138Ч139
On-the-fly model checking, partial order reduction      143 159 164 168
Orbit Problem      224Ч225
Orbit relation      222Ч223 226Ч228
Ordered Binary Decision Diagrams (OBDDs)      51Ч59
Ordered binary decision diagrams, $\mu$-calculus      104Ч107
Ordered binary decision diagrams, abstractions      196 203Ч204 210Ч211
Ordered binary decision diagrams, algorithms      66Ч95
Ordered binary decision diagrams, bisimulation      180
Ordered binary decision diagrams, boolean representation      51 53Ч57
1 2
       © Ёлектронна€ библиотека попечительского совета мехмата ћ√”, 2004-2024
Ёлектронна€ библиотека мехмата ћ√” | Valid HTML 4.01! | Valid CSS! ќ проекте