Preface |
|
xiii | |
|
|
1 | (16) |
|
|
2 | (4) |
|
|
6 | (2) |
|
|
8 | (7) |
|
|
15 | (2) |
|
I Modeling Dynamic Behaviors |
|
|
17 | (152) |
|
|
19 | (22) |
|
|
20 | (5) |
|
|
25 | (3) |
|
2.3 Properties of Systems |
|
|
28 | (3) |
|
|
31 | (6) |
|
|
37 | (4) |
|
|
37 | (4) |
|
|
41 | (34) |
|
|
42 | (4) |
|
|
46 | (1) |
|
3.3 Finite-State Machines |
|
|
47 | (9) |
|
3.4 Extended State Machines |
|
|
56 | (6) |
|
|
62 | (4) |
|
|
66 | (3) |
|
|
69 | (6) |
|
|
70 | (5) |
|
|
75 | (28) |
|
|
76 | (4) |
|
4.2 Classes of Hybrid Systems |
|
|
80 | (15) |
|
|
95 | (8) |
|
|
96 | (7) |
|
5 Composition of State Machines |
|
|
103 | (26) |
|
5.1 Concurrent Composition |
|
|
105 | (14) |
|
5.2 Hierarchical State Machines |
|
|
119 | (4) |
|
|
123 | (6) |
|
|
124 | (5) |
|
6 Concurrent Models of Computation |
|
|
129 | (40) |
|
|
130 | (2) |
|
6.2 Synchronous-Reactive Models |
|
|
132 | (10) |
|
6.3 Dataflow Models of Computation |
|
|
142 | (12) |
|
6.4 Timed Models of Computation |
|
|
154 | (9) |
|
|
163 | (6) |
|
|
163 | (6) |
|
II Design of Embedded Systems |
|
|
169 | (172) |
|
|
171 | (30) |
|
7.1 Models of Sensors and Actuators |
|
|
173 | (13) |
|
|
186 | (5) |
|
|
191 | (5) |
|
|
196 | (5) |
|
|
197 | (4) |
|
|
201 | (28) |
|
|
202 | (10) |
|
|
212 | (15) |
|
|
227 | (2) |
|
|
227 | (2) |
|
|
229 | (20) |
|
|
230 | (2) |
|
|
232 | (8) |
|
|
240 | (5) |
|
|
245 | (4) |
|
|
245 | (4) |
|
|
249 | (30) |
|
|
250 | (11) |
|
10.2 Sequential Software in a Concurrent World |
|
|
261 | (10) |
|
|
271 | (8) |
|
|
272 | (7) |
|
|
279 | (30) |
|
|
282 | (4) |
|
|
286 | (12) |
|
11.3 Processes and Message Passing |
|
|
298 | (5) |
|
|
303 | (6) |
|
|
304 | (5) |
|
|
309 | (32) |
|
12.1 Basics of Scheduling |
|
|
310 | (6) |
|
12.2 Rate Monotonic Scheduling |
|
|
316 | (4) |
|
12.3 Earliest Deadline First |
|
|
320 | (5) |
|
12.4 Scheduling and Mutual Exclusion |
|
|
325 | (4) |
|
12.5 Multiprocessor Scheduling |
|
|
329 | (6) |
|
|
335 | (6) |
|
|
335 | (6) |
|
III Analysis and Verification |
|
|
341 | (128) |
|
13 Invariants and Temporal Logic |
|
|
343 | (16) |
|
|
344 | (2) |
|
13.2 Linear Temporal Logic |
|
|
346 | (8) |
|
|
354 | (5) |
|
|
356 | (3) |
|
14 Equivalence and Refinement |
|
|
359 | (26) |
|
14.1 Models as Specifications |
|
|
360 | (1) |
|
14.2 Type Equivalence and Refinement |
|
|
361 | (3) |
|
14.3 Language Equivalence and Containment |
|
|
364 | (6) |
|
|
370 | (7) |
|
|
377 | (2) |
|
|
379 | (6) |
|
|
380 | (5) |
|
15 Reachability Analysis and Model Checking |
|
|
385 | (22) |
|
15.1 Open and Closed Systems |
|
|
386 | (1) |
|
15.2 Reachability Analysis |
|
|
387 | (7) |
|
15.3 Abstraction in Model Checking |
|
|
394 | (3) |
|
15.4 Model Checking Liveness Properties |
|
|
397 | (6) |
|
|
403 | (4) |
|
|
405 | (2) |
|
|
407 | (30) |
|
16.1 Problems of Interest |
|
|
408 | (2) |
|
|
410 | (5) |
|
16.3 Factors Determining Execution Time |
|
|
415 | (6) |
|
16.4 Basics of Execution Time Analysis |
|
|
421 | (10) |
|
16.5 Other Quantitative Analysis Problems |
|
|
431 | (1) |
|
|
432 | (5) |
|
|
433 | (4) |
|
|
437 | (32) |
|
17.1 Cryptographic Primitives |
|
|
439 | (7) |
|
17.2 Protocol and Network Security |
|
|
446 | (5) |
|
|
451 | (3) |
|
|
454 | (8) |
|
|
462 | (5) |
|
|
467 | (2) |
|
|
467 | (2) |
|
|
469 | (2) |
|
|
471 | (8) |
|
|
471 | (1) |
|
A.2 Relations and Functions |
|
|
472 | (4) |
|
|
476 | (3) |
|
|
478 | (1) |
|
B Complexity and Computability |
|
|
479 | (18) |
|
B.1 Effectiveness and Complexity of Algorithms |
|
|
480 | (3) |
|
B.2 Problems, Algorithms, and Programs |
|
|
483 | (2) |
|
B.3 Turing Machines and Undecidability |
|
|
485 | (6) |
|
B.4 Intractability: P and NP |
|
|
491 | (3) |
|
|
494 | (3) |
|
|
494 | (3) |
Bibliography |
|
497 | (18) |
Notation Index |
|
515 | (2) |
Index |
|
517 | |