Copyright ⃝c 2011-2012 Edward Ashford Lee & Sanjit Arunkumar Seshia All rights reserved First Edition, Version 1.06 ISBN 978-0-557-70857-4 Please cite this book as: E. A. Lee and S. A. Seshia, Introduction to Embedded Systems - A Cyber-Physical Systems Approach, LeeSeshia.org, 2011. This book is dedicated to our families. Contents Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xi 1 Introduction 1 1.1 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 The Design Process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 I Modeling Dynamic Behaviors 17 2 Continuous Dynamics 19 2.1 Newtonian Mechanics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.2 Actor Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.3 Properties of Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4 Feedback Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 v 3 Discrete Dynamics 41 3.1 Discrete Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2 The Notion of State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.3 Finite-State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.4 Extended State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.5 Nondeterminism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.6 Behaviors and Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 3.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4 Hybrid Systems 77 4.1 Modal Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 4.2 Classes of Hybrid Systems . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 5 Composition of State Machines 107 5.1 Concurrent Composition . . . . . . . . . . . . . . . . . . . . . . . . . . 109 5.2 Hierarchical State Machines . . . . . . . . . . . . . . . . . . . . . . . . 123 5.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 6 Concurrent Models of Computation 131 6.1 Structure of Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 6.2 Synchronous-Reactive Models . . . . . . . . . . . . . . . . . . . . . . . 134 6.3 Dataflow Models of Computation . . . . . . . . . . . . . . . . . . . . . . 144 6.4 Timed Models of Computation . . . . . . . . . . . . . . . . . . . . . . . 156 6.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167 vi Lee & Seshia, Introduction to Embedded Systems II Design of Embedded Systems 173 7 Embedded Processors 175 7.1 Types of Processors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 7.2 Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 7.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 8 Memory Architectures 203 8.1 Memory Technologies . . . . . . . . . . . . . . . . . . . . . . . . . . . 204 8.2 Memory Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206 8.3 Memory Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 8.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221 9 Input and Output 223 9.1 I/O Hardware . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224 9.2 Sequential Software in a Concurrent World . . . . . . . . . . . . . . . . 236 9.3 The Analog/Digital Interface . . . . . . . . . . . . . . . . . . . . . . . . 246 9.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256 10 Multitasking 265 10.1 Imperative Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 268 10.2 Threads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 272 10.3 Processes and Message Passing . . . . . . . . . . . . . . . . . . . . . . . 285 10.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 291 11 Scheduling 293 11.1 Basics of Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . . . . 294 Lee & Seshia, Introduction to Embedded Systems vii 11.2 Rate Monotonic Scheduling . . . . . . . . . . . . . . . . . . . . . . . . 300 11.3 Earliest Deadline First . . . . . . . . . . . . . . . . . . . . . . . . . . . 305 11.4 Scheduling and Mutual Exclusion . . . . . . . . . . . . . . . . . . . . . 310 11.5 Multiprocessor Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . 315 11.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 321 III Analysis and Verification 327 12 Invariants and Temporal Logic 329 12.1 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 331 12.2 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 333 12.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343 13 Equivalence and Refinement 347 13.1 Models as Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . 348 13.2 Type Equivalence and Refinement . . . . . . . . . . . . . . . . . . . . . 350 13.3 Language Equivalence and Containment . . . . . . . . . . . . . . . . . . 352 13.4 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 13.5 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 366 13.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 369 14 Reachability Analysis and Model Checking 373 14.1 Open and Closed Systems . . . . . . . . . . . . . . . . . . . . . . . . . 374 14.2 Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 376 14.3 Abstraction in Model Checking . . . . . . . . . . . . . . . . . . . . . . . 383 14.4 Model Checking Liveness Properties . . . . . . . . . . . . . . . . . . . . 386 14.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391 viii Lee & Seshia, Introduction to Embedded Systems Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394 15 Quantitative Analysis 395 15.1 Problems of Interest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397 15.2 Programs as Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399 15.3 Factors Determining Execution Time . . . . . . . . . . . . . . . . . . . . 404 15.4 Basics of Execution Time Analysis . . . . . . . . . . . . . . . . . . . . . 410 15.5 Other Quantitative Analysis Problems . . . . . . . . . . . . . . . . . . . 419 15.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 IV Appendices 425 A Sets and Functions 427 A.1 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 A.2 Relations and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 428 A.3 Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 435 B Complexity and Computability 437 B.1 Effectiveness and Complexity of Algorithms . . . . . . . . . . . . . . . . 438 B.2 Problems, Algorithms, and Programs . . . . . . . . . . . . . . . . . . . . 441 B.3 Turing Machines and Undecidability . . . . . . . . . . . . . . . . . . . . 443 B.4 Intractability: P and NP . . . . . . . . . . . . . . . . . . . . . . . . . . . 449 B.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 Bibliography 455 Notation Index 471 Index 473 Lee & Seshia, Introduction to Embedded Systems ix x Lee & Seshia, Introduction to Embedded Systems