Preface......Page 11
Introduction......Page 23
Applications......Page 24
Motivating Example......Page 28
The Design Process......Page 30
Summary......Page 37
I Modeling Dynamic Behaviors......Page 39
Continuous Dynamics......Page 41
Newtonian Mechanics......Page 42
Actor Models......Page 47
Properties of Systems......Page 51
Feedback Control......Page 54
Summary......Page 60
Exercises......Page 61
Discrete Dynamics......Page 65
Discrete Systems......Page 66
The Notion of State......Page 71
Finite-State Machines......Page 72
Extended State Machines......Page 81
Nondeterminism......Page 87
Behaviors and Traces......Page 91
Summary......Page 94
Exercises......Page 96
Hybrid Systems......Page 101
Modal Models......Page 102
Classes of Hybrid Systems......Page 106
Summary......Page 123
Exercises......Page 125
Composition of State Machines......Page 131
Concurrent Composition......Page 133
Hierarchical State Machines......Page 146
Summary......Page 151
Exercises......Page 153
Concurrent Models of Computation......Page 155
Structure of Models......Page 157
Synchronous-Reactive Models......Page 158
Dataflow Models of Computation......Page 167
Timed Models of Computation......Page 181
Summary......Page 190
Exercises......Page 192
II Design of Embedded Systems......Page 197
Embedded Processors......Page 199
Types of Processors......Page 201
Parallelism......Page 208
Summary......Page 226
Exercises......Page 227
Memory Architectures......Page 229
Memory Technologies......Page 230
Memory Hierarchy......Page 233
Memory Models......Page 242
Summary......Page 246
Exercises......Page 248
Input and Output......Page 251
I/O Hardware......Page 252
Sequential Software in a Concurrent World......Page 264
The Analog/Digital Interface......Page 275
Summary......Page 284
Exercises......Page 285
Multitasking......Page 293
Imperative Programs......Page 296
Threads......Page 300
Processes and Message Passing......Page 313
Summary......Page 319
Exercises......Page 320
Scheduling......Page 323
Basics of Scheduling......Page 324
Rate Monotonic Scheduling......Page 331
Earliest Deadline First......Page 335
Scheduling and Mutual Exclusion......Page 340
Multiprocessor Scheduling......Page 345
Summary......Page 349
Exercises......Page 351
III Analysis and Verification......Page 355
Invariants and Temporal Logic......Page 357
Invariants......Page 359
Linear Temporal Logic......Page 361
Summary......Page 369
Exercises......Page 371
Equivalence and Refinement......Page 375
Models as Specifications......Page 376
Type Equivalence and Refinement......Page 378
Language Equivalence and Containment......Page 380
Simulation......Page 386
Bisimulation......Page 394
Summary......Page 397
Exercises......Page 398
Reachability Analysis and Model Checking......Page 403
Open and Closed Systems......Page 404
Reachability Analysis......Page 406
Abstraction in Model Checking......Page 413
Model Checking Liveness Properties......Page 416
Summary......Page 421
Exercises......Page 424
Quantitative Analysis......Page 427
Problems of Interest......Page 429
Programs as Graphs......Page 431
Factors Determining Execution Time......Page 436
Basics of Execution Time Analysis......Page 442
Other Quantitative Analysis Problems......Page 451
Summary......Page 454
Exercises......Page 455
IV Appendices......Page 457
Sets......Page 459
Relations and Functions......Page 460
Sequences......Page 464
Exercises......Page 467
Complexity and Computability......Page 469
Effectiveness and Complexity of Algorithms......Page 470
Problems, Algorithms, and Programs......Page 473
Turing Machines and Undecidability......Page 476
Intractability: P and NP......Page 482
Summary......Page 485
Exercises......Page 486
Bibliography......Page 489
Notation Index......Page 505
Index......Page 507