Ãëàâíàÿ    Ex Libris    Êíèãè    Æóðíàëû    Ñòàòüè    Ñåðèè    Êàòàëîã    Wanted    Çàãðóçêà    ÕóäËèò    Ñïðàâêà    Ïîèñê ïî èíäåêñàì    Ïîèñê    Ôîðóì   
blank
Àâòîðèçàöèÿ

       
blank
Ïîèñê ïî óêàçàòåëÿì

blank
blank
blank
Êðàñîòà
blank
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
blank
Ïðåäìåòíûé óêàçàòåëü
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
1 2
blank
Ðåêëàìà
blank
blank
HR
@Mail.ru
       © Ýëåêòðîííàÿ áèáëèîòåêà ïîïå÷èòåëüñêîãî ñîâåòà ìåõìàòà ÌÃÓ, 2004-2024
Ýëåêòðîííàÿ áèáëèîòåêà ìåõìàòà ÌÃÓ | Valid HTML 4.01! | Valid CSS! Î ïðîåêòå