Àâòîðèçàöèÿ
Ïîèñê ïî óêàçàòåëÿì
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
Ïðåäìåòíûé óêàçàòåëü
Ordered binary decision diagrams, future research on 293 Ordered binary decision diagrams, introduction to 7—8 Ordered binary decision diagrams, Kripke structures, encoding of 51 57—59 Ordered binary decision diagrams, logical operations 55—57 Ordered binary decision diagrams, ordering selection, heuristics for 54—55 Ordered binary decision diagrams, ordering selection, partitioning and 82—85 Ordered binary decision diagrams, partitioned transition relations 79—85 Ordered binary decision diagrams, size of 53—54 84 226—228 Ordered binary decision diagrams, symmetry 222—223 226—228 Parallel composition 187 188—189 268—269 Parameterized designs 231 see Partial order reduction 141—170 Partial order reduction, ample set calculation 144 154—160 Partial order reduction, ample set selection 147—151 154—155 Partial order reduction, asynchronous system concurrency 142—144 Partial order reduction, commutativity 144—145 147 Partial order reduction, correctness 160—164 Partial order reduction, dependency relation 141 144—145 157 Partial order reduction, future research on 294 Partial order reduction, independence relation 144—145 Partial order reduction, introduction to 8—9 Partial order reduction, invisibility 145 147 149—150 Partial order reduction, LTL 146—154 159 164 Partial order reduction, SPIN system 159 164—170 Partial order reduction, stuttering equivalence 146—154 163—164 Partial order reduction, usefulness of xiv 141 Partitioned transition relations 79—87 Passable guard 165 Path formulas 28—29 Path quantifiers 27 Permutation groups 215—216 Persistent sets 9 Point-to-point networks, arbitrary 294 Positive normal form 31 Predicate transformers 7 61—66 Preorder, simulation 176—180 188—189 232—234 Present state variables 15 Preservation, strong and weak 232 Priority inversion 259 262—264 Probablistic verification 295 Process 22 24 Process synchronization 24 Program counter 21 156 Programs, concurrent 22—24 Programs, sequential 20—22 Programs, translation example 24—26 PROMELA language 164—168 Proof systems xiii 3 295 see PSPACE-completeness 6 41 180 Pushing inward, and data abstraction 200—202 QUANTIFIED BOOLEAN FORMULAS 66—67 Quantitative temporal analysis 256—264 Quotient models 218—221 222—223 Quotient structure 218—219 Rate-monotonic scheduling (RMS) 253—254 261 Reachability 154 268—292 Reactive systems 13 27 Real-time systems 253—292 Real-time systems, clock regions 274—280 Real-time systems, clock zones 280—291 Real-time systems, complexity 291—292 Real-time systems, continuous 265—292 Real-time systems, difference bound matrices 283 287—291 Real-time systems, discrete 254 255—264 265 Real-time systems, examples 259—264 269—273 Real-time systems, future research on 294 Real-time systems, limitations on checking of 254 Real-time systems, parallel composition 268—269 Real-time systems, quantitative temporal analysis 256—264 Real-time systems, region graph 279—280 291 Real-time systems, RMS theory 253—254 261 Real-time systems, RTCTL model checking 255—256 Real-time systems, timed automata 265—291 Reduced state graph 143 see Region graph 279—280 291 Relational product 77—87 Release operator 28 Representatives 141 see Restricted path formula 41 87 Result cache 56 RMS (rate-monotonic scheduling) 253—254 261 Rotation groups 226—228 RTCTL model checking 255—256 SCCs (strongly connected components) 36 44 129 Schedulability 253 254 255 262—264 see Security protocols 3 Self-fulfilling SCC 44 Sequential composition statement 22 Sequential programs 20—22 Shannon expansion 55—56 SHARED variables 17 24 Simulation preorder 176—180 188—189 232—234 Simulation relation 176 Simulation, method of xi xiii 2 Single bit abstraction 208—210 SKIP statement 21 Sleep sets 9 SMV (Symbolic Model Verifier) 7 8 109—120 SMV, example 112—120 SMV, features 109—112 snarfing 114 Solvability see "Undecidability" Specification, as step in model checking 4 Spin system 159 164—170 Square meshes 294 State explosion 9 10—11 State explosion, challenge of xiii 1 8 State explosion, concurrent events, all orderings of 142 State explosion, continuous real time 292 State formulas 28—29 State holding element 17 State transition system 141 States 13 14—15 See Static time-slicing 253 String, as sequence of transitions 160 Strong preservation 232 Strongly connected components (SCCs) 36 44 129 Stubborn sets 9 Stuttering equivalence 146—154 163—164 Subgroups 215 Suffix 29 Symbolic abstractions 210—213 Symbolic model checking xii 61—95 Symbolic model checking, counterexamples 71—74 Symbolic model checking, CTL 66—87 Symbolic model checking, efficiency 80—87 Symbolic model checking, example 75—77 85—87 Symbolic model checking, fairness 68—71 72—74 91—95 Symbolic model checking, fixpoint representations 61—66 Symbolic model checking, introduction to 6—8 Symbolic model checking, LTL 87—95 Symbolic model checking, partial order reduction 143 Symbolic model checking, partitioned transition relations 79—87 Symbolic model checking, real-time systems 254 255 291 Symbolic model checking, relational product 77—87 Symbolic model checking, symmetry 228 Unlock statement 24 Until operator 28 Valuation function 14 Verification see also "Model checking" Verification, methods of xi 1—3 Verification, need for xi—xii 1—2 Verification, probabilistic 295 Vertices, in binary decision trees 51—52 VERUS 261—264 Visibility 145 162 Wait statement 24 Weak preservation 232 while statement 22 witnesses 71—74 see Zone graph 283—284 289 Zones 283 see
Ðåêëàìà
|
|
Î ïðîåêòå