Introduction to Embedded Systems A Cyber-Physical Systems Approach Second Edition Edward Ashford Lee Sanjit Arunkumar Seshia Copyright ⃝c 2011-2015 Edward Ashford Lee & Sanjit Arunkumar Seshia All rights reserved Second Edition, Version 2.0 ISBN 978-1-312-42740-2 Please cite this book as: E. A. Lee and S. A. Seshia, Introduction to Embedded Systems - A Cyber-Physical Systems Approach, Second Edition, LeeSeshia.org, 2015. 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 43 3.1 Discrete Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.2 The Notion of State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.3 Finite-State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.4 Extended State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . 59 3.5 Nondeterminism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 3.6 Behaviors and Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 3.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4 Hybrid Systems 79 4.1 Modal Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 4.2 Classes of Hybrid Systems . . . . . . . . . . . . . . . . . . . . . . . . . 83 4.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 5 Composition of State Machines 109 5.1 Concurrent Composition . . . . . . . . . . . . . . . . . . . . . . . . . . 111 5.2 Hierarchical State Machines . . . . . . . . . . . . . . . . . . . . . . . . 126 5.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 6 Concurrent Models of Computation 135 6.1 Structure of Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 6.2 Synchronous-Reactive Models . . . . . . . . . . . . . . . . . . . . . . . 141 6.3 Dataflow Models of Computation . . . . . . . . . . . . . . . . . . . . . . 147 6.4 Timed Models of Computation . . . . . . . . . . . . . . . . . . . . . . . 161 6.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171 vi Lee & Seshia, Introduction to Embedded Systems II Design of Embedded Systems 177 7 Sensors and Actuators 179 7.1 Models of Sensors and Actuators . . . . . . . . . . . . . . . . . . . . . . 181 7.2 Common Sensors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 7.3 Actuators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200 7.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206 8 Embedded Processors 209 8.1 Types of Processors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210 8.2 Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219 8.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 9 Memory Architectures 239 9.1 Memory Technologies . . . . . . . . . . . . . . . . . . . . . . . . . . . 240 9.2 Memory Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242 9.3 Memory Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 251 9.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257 10 Input and Output 261 10.1 I/O Hardware . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 262 10.2 Sequential Software in a Concurrent World . . . . . . . . . . . . . . . . 273 10.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 282 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 285 11 Multitasking 293 11.1 Imperative Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 296 11.2 Threads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 11.3 Processes and Message Passing . . . . . . . . . . . . . . . . . . . . . . . 313 Lee & Seshia, Introduction to Embedded Systems vii 11.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 318 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319 12 Scheduling 321 12.1 Basics of Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322 12.2 Rate Monotonic Scheduling . . . . . . . . . . . . . . . . . . . . . . . . 328 12.3 Earliest Deadline First . . . . . . . . . . . . . . . . . . . . . . . . . . . 333 12.4 Scheduling and Mutual Exclusion . . . . . . . . . . . . . . . . . . . . . 338 12.5 Multiprocessor Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . 343 12.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 347 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 349 III Analysis and Verification 355 13 Invariants and Temporal Logic 357 13.1 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 358 13.2 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 360 13.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371 14 Equivalence and Refinement 375 14.1 Models as Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . 376 14.2 Type Equivalence and Refinement . . . . . . . . . . . . . . . . . . . . . 377 14.3 Language Equivalence and Containment . . . . . . . . . . . . . . . . . . 380 14.4 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 386 14.5 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394 14.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397 15 Reachability Analysis and Model Checking 403 viii Lee & Seshia, Introduction to Embedded Systems 15.1 Open and Closed Systems . . . . . . . . . . . . . . . . . . . . . . . . . 404 15.2 Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 406 15.3 Abstraction in Model Checking . . . . . . . . . . . . . . . . . . . . . . . 413 15.4 Model Checking Liveness Properties . . . . . . . . . . . . . . . . . . . . 416 15.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424 16 Quantitative Analysis 427 16.1 Problems of Interest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 429 16.2 Programs as Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431 16.3 Factors Determining Execution Time . . . . . . . . . . . . . . . . . . . . 436 16.4 Basics of Execution Time Analysis . . . . . . . . . . . . . . . . . . . . . 442 16.5 Other Quantitative Analysis Problems . . . . . . . . . . . . . . . . . . . 451 16.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 17 Security and Privacy 459 17.1 Cryptographic Primitives . . . . . . . . . . . . . . . . . . . . . . . . . . 461 17.2 Protocol and Network Security . . . . . . . . . . . . . . . . . . . . . . . 469 17.3 Software Security . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474 17.4 Information Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 17.5 Advanced Topics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486 17.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 490 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492 IV Appendices 493 A Sets and Functions 495 A.1 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 495 A.2 Relations and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 496 Lee & Seshia, Introduction to Embedded Systems ix A.3 Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 500 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 503 B Complexity and Computability 505 B.1 Effectiveness and Complexity of Algorithms . . . . . . . . . . . . . . . . 506 B.2 Problems, Algorithms, and Programs . . . . . . . . . . . . . . . . . . . . 509 B.3 Turing Machines and Undecidability . . . . . . . . . . . . . . . . . . . . 511 B.4 Intractability: P and NP . . . . . . . . . . . . . . . . . . . . . . . . . . . 517 B.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 521 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 522 Bibliography 523 Notation Index 542 Index 545 x Lee & Seshia, Introduction to Embedded Systems