Abstract In distributed systems with processes that do not share a global clock, partial synchrony is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an approximate distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.

IoT (Internet of Things) applications often involve stream processing using multiple complex layers of processing nodes, where in each layer, data is received by the nodes, processed, and then transmitted to the nodes in subsequent layers. Such systems present a tradeoff between reliability and resource usage, including CPU power, energy, network band-width, memory, etc. Reducing the reliability at which a node processes inbound data in a layer can have repercussions on nodes in subsequent layers in the network that receive less reliable data, and in turn impact the reliability of the application as a whole. In this paper, we present a generalized model of streaming IoT applications as a layered network of producers and consumers. Our model captures trade-offs between reliability and resource usage of the system. We present an efficient algorithm using SMT constraint solvers to determine the optimal selection of processing quality for each node in the 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 drastically improve our model in terms of run time. We have fully implemented our technique and report experimental results on a layered IoT network.

Cyber-physical systems (CPS) are computer systems with integrated software and physical components that ideally seamlessly interact with the real world and each other. While the use of distributed CPS has rapidly grown over the past decade, so has the need for developing efficient methods to ascertain reliability of these systems by validating their correctness. Since exhaustively validating correctness of a distributed CPS is usually not feasible nor possible, many modern validation methods involve run-time verification of distributed CPS based on safety properties. Our work focuses on developing time and resource efficient assurance techniques that can run in parallel with the execution of these systems to ensure reliability.

In this paper, we study the problem of runtime verification of distributed applications that do not share a global clock with respect to specifications in the linear temporal logics (LTL). Our proposed method distinguishes from the existing work in three novel ways. First, we make a practical assumption that the distributed system under scrutiny is augmented with a clock synchronization algorithm that guarantees bounded clock skew among all processes. Second, we do not make any assumption about the structure of predicates that form LTL formulas. This relaxation allows us to monitor a wide range of applications that was not possible before. Subsequently, we propose a distributed monitoring algorithm by employing SMT solving techniques. Third, given the fact that distributed applications nowadays run on massive cloud services, we extend our solution to a parallel monitoring algorithm to utilize the available computing infrastructure. We report on rigorous synthetic as well as real-world case studies and demonstrate that scalable online monitoring of distributed applications is within our reach.