This dissertation addresses the problem of runtime verification of distributed cyber-physical systems (CPS) with respect to a given formal specification. Cyber-physical systems are computer systems with integrated software and physical (hardware) components that, in an ideal environment, seamlessly interact with the real world, as well as each other. Since exhaustively validating correctness of a distributed CPS is usually infeasible (if not impossible), many modern validation methods involve runtime verification of distributed CPS based on safety properties. Our work focuses on developing time efficient and resource efficient verification techniques that can run in parallel with the execution of these systems to ensure reliability.In this dissertation, we propose different methodologies to reason about the correctness of distributed CPS in real-time, depending on the system settings and architecture. We also provide case studies relevant to each approach in order to demonstrate real-world applications. In all our proposed techniques, we assume a partially synchronous setting, where a clock synchronization algorithm guarantees a bound on clock drifts among all signals. To this end, we first introduce two monitoring methods for distributed systems with discrete events, where the specification in the linear temporal logic (LTL) is evaluated on a system using (1) a deterministic finite automaton-based technique, and (2) a progression-based formula rewriting technique. We then extend this work to detecting violations of predicates over distributed continuous-time and continuous-valued signals in CPS. We introduce a novel retiming technique that allows reasoning about the correctness of predicates among continuous-time signals that do not share a global view of time. In addition, we show that leveraging simple knowledge of physical dynamics allows for further reduction in run time. Leveraging the previous two methods, we then introduce a monitoring technique for solving the problem of runtime verification for distributed CPS using the signal temporal logic (STL). We employ a formula progression technique utilizing a signal retiming method, that enables reasoning about the correctness of formulas among continuous-time and continuous-valued signals in CPS, even when only a partial signal is available. We also extend our previous work on detecting violations of predicates over distributed signals in CPS from a centralized monitoring setting to a decentralized monitoring setting. We employ a technique that allows us to indentify all possible violations, not just one. Which in turn allows for identification and elimination of bugs from distributed systems regardless of the actual clock drift. Finally, we introduce the notion of monitoring reliability on a network of monitors in decentralized monitoring setting. To this end, we present a generalized model of a class of CPS, where each monitor is represented by an Internet of Things (IoT) device (or node) in a layered network of producers and consumers. Our model monitors the events in nodes where resource usage occurs, and captures the tradeoffs between the reliability of the system and resource usage. We present an efficient algorithm to determine the optimal selection of processing quality for each node in this producer-consumer network, such that target system reliability is achieved while respecting the given resource bounds, and resource usage is minimized. In addition, we present a lightweight machine learning based solution to improve our model in terms of run time.
Read
