Principles of Cyber-Physical Systems Principles of Cyber-Physical Systems Rajeev Alur The MIT Press Cambridge, Massachusetts London, England (cid:2)c 2015 Massachusetts Institute of Technology Allrightsreserved. Nopartofthisbookmaybereproducedinanyformbyany electronic or mechanical means (including photocopying, recording, or informa- tion storage and retrieval) without permission in writing from the publisher. MITPressbooksmaybepurchasedatspecialquantitydiscountsforbusinessor salespromotionaluse. Forinformation,pleaseemailspecial [email protected]. ThisbookwassetusingLATEXbytheauthor. PrintedandboundintheUnited States of America. Library of Congress Cataloging-in-Publication Data Alur, Rajeev, 1966– Principles of cyber-physical systems / Rajeev Alur. p. cm Includes bibliographical references and index. ISBN: 978-0-262-02911-7 (hardcover: alk. paper) 1. Automatic control. 2. System design. 3. Embedded internet devices. 4. Internet of things. 5. Formal methods (Computer science). I. Title. TJ213.A365 2015 006.2’2—dc23 2014039755 Dedicated to the memory of my parents Contents Preface xi 1 Introduction 1 1.1 What Is a Cyber-Physical System? . . . . . . . . . . . . . . . . . 1 1.2 Key Features of Cyber-Physical Systems . . . . . . . . . . . . . . 2 1.3 Overview of Topics . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Guide to Course Organization . . . . . . . . . . . . . . . . . . . . 7 2 Synchronous Model 13 2.1 Reactive Components . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.1 Variables, Valuations, and Expressions . . . . . . . . . . . 13 2.1.2 Inputs, Outputs, and States . . . . . . . . . . . . . . . . . 14 2.1.3 Initialization . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.1.4 Update . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.1.5 Executions . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.1.6 Extended-State Machines . . . . . . . . . . . . . . . . . . 19 2.2 Properties of Components . . . . . . . . . . . . . . . . . . . . . . 21 2.2.1 Finite-State Components . . . . . . . . . . . . . . . . . . 21 2.2.2 Combinational Components . . . . . . . . . . . . . . . . . 22 2.2.3 Event-Triggered Components∗ . . . . . . . . . . . . . . . 24 2.2.4 Nondeterministic Components . . . . . . . . . . . . . . . 26 2.2.5 Input-Enabled Components . . . . . . . . . . . . . . . . . 29 2.2.6 Task Graphs and Await Dependencies . . . . . . . . . . . 30 2.3 Composing Components . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.1 Block Diagrams. . . . . . . . . . . . . . . . . . . . . . . . 36 2.3.2 Input/Output Variable Renaming . . . . . . . . . . . . . 38 2.3.3 Parallel Composition . . . . . . . . . . . . . . . . . . . . . 38 2.3.4 Output Hiding . . . . . . . . . . . . . . . . . . . . . . . . 47 2.4 Synchronous Designs . . . . . . . . . . . . . . . . . . . . . . . . . 49 2.4.1 Synchronous Circuits. . . . . . . . . . . . . . . . . . . . . 50 2.4.2 Cruise Control System . . . . . . . . . . . . . . . . . . . . 54 2.4.3 Synchronous Networks∗ . . . . . . . . . . . . . . . . . . . 58 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 viii Contents 3 Safety Requirements 65 3.1 Safety Specifications . . . . . . . . . . . . . . . . . . . . . . . . . 65 3.1.1 Invariants of Transition Systems . . . . . . . . . . . . . . 65 3.1.2 Role of Requirements in System Design . . . . . . . . . . 70 3.1.3 Safety Monitors. . . . . . . . . . . . . . . . . . . . . . . . 75 3.2 Verifying Invariants. . . . . . . . . . . . . . . . . . . . . . . . . . 78 3.2.1 Proving Invariants . . . . . . . . . . . . . . . . . . . . . . 78 3.2.2 Automated Invariant Verification∗ . . . . . . . . . . . . . 85 3.2.3 Simulation-Based Analysis. . . . . . . . . . . . . . . . . . 87 3.3 Enumerative Search∗ . . . . . . . . . . . . . . . . . . . . . . . . . 90 3.4 Symbolic Search . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 3.4.1 Symbolic Transition Systems . . . . . . . . . . . . . . . . 98 3.4.2 Symbolic Breadth-First Search . . . . . . . . . . . . . . . 103 3.4.3 Reduced Ordered Binary Decision Diagrams∗ . . . . . . . 109 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 4 Asynchronous Model 125 4.1 Asynchronous Processes . . . . . . . . . . . . . . . . . . . . . . . 125 4.1.1 States, Inputs, and Outputs . . . . . . . . . . . . . . . . . 126 4.1.2 Input, Output, and Internal Actions . . . . . . . . . . . . 126 4.1.3 Executions . . . . . . . . . . . . . . . . . . . . . . . . . . 131 4.1.4 Extended-State Machines . . . . . . . . . . . . . . . . . . 132 4.1.5 Operations on Processes . . . . . . . . . . . . . . . . . . . 136 4.1.6 Safety Requirements . . . . . . . . . . . . . . . . . . . . . 141 4.2 Asynchronous Design Primitives . . . . . . . . . . . . . . . . . . 142 4.2.1 Blocking vs. Non-blocking Synchronization . . . . . . . . 142 4.2.2 Deadlocks . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 4.2.3 Shared Memory. . . . . . . . . . . . . . . . . . . . . . . . 145 4.2.4 Fairness Assumptions∗ . . . . . . . . . . . . . . . . . . . . 154 4.3 Asynchronous Coordination Protocols . . . . . . . . . . . . . . . 162 4.3.1 Leader Election . . . . . . . . . . . . . . . . . . . . . . . 163 4.3.2 Reliable Transmission . . . . . . . . . . . . . . . . . . . . 167 4.3.3 Wait-Free Consensus∗ . . . . . . . . . . . . . . . . . . . . 170 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179 5 Liveness Requirements 181 5.1 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181 5.1.1 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . 182 5.1.2 Ltl Specifications . . . . . . . . . . . . . . . . . . . . . . 189 5.1.3 Ltl Specifications for Asynchronous Processes∗ . . . . . . 193 5.1.4 Beyond Ltl∗ . . . . . . . . . . . . . . . . . . . . . . . . . 197 5.2 Model Checking. . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 5.2.1 Bu¨chi Automata . . . . . . . . . . . . . . . . . . . . . . . 200 5.2.2 From Ltl to Bu¨chi Automata∗ . . . . . . . . . . . . . . . 206 5.2.3 Nested Depth-First Search∗ . . . . . . . . . . . . . . . . . 212 5.2.4 Symbolic Repeatability Checking . . . . . . . . . . . . . . 216 Contents ix 5.3 Proving Liveness∗ . . . . . . . . . . . . . . . . . . . . . . . . . . 222 5.3.1 Eventuality Properties . . . . . . . . . . . . . . . . . . . . 222 5.3.2 Conditional Response Properties . . . . . . . . . . . . . . 224 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229 6 Dynamical Systems 231 6.1 Continuous-Time Models . . . . . . . . . . . . . . . . . . . . . . 231 6.1.1 Continuously Evolving Inputs and Outputs . . . . . . . . 231 6.1.2 Models with Disturbance . . . . . . . . . . . . . . . . . . 241 6.1.3 Composing Components . . . . . . . . . . . . . . . . . . . 242 6.1.4 Stability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243 6.2 Linear Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 6.2.1 Linearity . . . . . . . . . . . . . . . . . . . . . . . . . . . 248 6.2.2 Solutions of Linear Differential Equations . . . . . . . . . 251 6.2.3 Stability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 6.3 Designing Controllers. . . . . . . . . . . . . . . . . . . . . . . . . 263 6.3.1 Open-Loop vs. Feedback Controller . . . . . . . . . . . . 263 6.3.2 Stabilizing Controller . . . . . . . . . . . . . . . . . . . . 264 6.3.3 PID Controllers∗ . . . . . . . . . . . . . . . . . . . . . . . 269 6.4 Analysis Techniques∗ . . . . . . . . . . . . . . . . . . . . . . . . 276 6.4.1 Numerical Simulation . . . . . . . . . . . . . . . . . . . . 277 6.4.2 Barrier Certificates . . . . . . . . . . . . . . . . . . . . . . 280 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 7 Timed Model 289 7.1 Timed Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 7.1.1 Timing-Based Light Switch . . . . . . . . . . . . . . . . . 289 7.1.2 Buffer with a Bounded Delay . . . . . . . . . . . . . . . . 291 7.1.3 Multiple Clocks . . . . . . . . . . . . . . . . . . . . . . . . 292 7.1.4 Formal Model . . . . . . . . . . . . . . . . . . . . . . . . . 294 7.1.5 Timed Process Composition . . . . . . . . . . . . . . . . . 297 7.1.6 Modeling Imperfect Clocks∗ . . . . . . . . . . . . . . . . . 300 7.2 Timing-Based Protocols . . . . . . . . . . . . . . . . . . . . . . . 301 7.2.1 Timing-Based Distributed Coordination . . . . . . . . . . 302 7.2.2 Audio Control Protocol∗ . . . . . . . . . . . . . . . . . . 305 7.2.3 Dual Chamber Implantable Pacemaker . . . . . . . . . . . 310 7.3 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 317 7.3.1 Model of Timed Automata . . . . . . . . . . . . . . . . . 318 7.3.2 Region Equivalence∗ . . . . . . . . . . . . . . . . . . . . . 319 7.3.3 Matrix-Based Representation for Symbolic Analysis . . . 328 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 338