Àâòîðèçàöèÿ
Ïîèñê ïî óêàçàòåëÿì
Clarke E.M., Grumberg O., Peled D.A. — Model checking
Îáñóäèòå êíèãó íà íàó÷íîì ôîðóìå Íàøëè îïå÷àòêó?
Íàçâàíèå: 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.
ßçûê: Ðóáðèêà: Òåõíîëîãèÿ /Ñòàòóñ ïðåäìåòíîãî óêàçàòåëÿ: Ãîòîâ óêàçàòåëü ñ íîìåðàìè ñòðàíèö ed2k: ed2k stats Ãîä èçäàíèÿ: 2000Êîëè÷åñòâî ñòðàíèö: 314Äîáàâëåíà â êàòàëîã: 04.12.2005Îïåðàöèè: Ïîëîæèòü íà ïîëêó |
Ñêîïèðîâàòü ññûëêó äëÿ ôîðóìà | Ñêîïèðîâàòü ID
Ïðåäìåòíûé óêàçàòåëü
69 97—108 101 103 108 107—108 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 BREADTH FIRST SEARCH 143 155 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, 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, 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, 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
Ðåêëàìà
-calculus 
|
|
Î ïðîåêòå