Abstract We introduce the tool $$^{\textsf {\small 2.0}}$$ 2 . 0 , the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line, standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

Abstract Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability to reach an error state is above a threshold? We consider an understudied extension that relates different reachability probabilities, such as: Is there a scheduler such that two sets of states are reached with different probabilities? These questions appear naturally in the design of randomized algorithms and in various security applications. We provide a tractable algorithm for many variations of this problem, while proving computational hardness of some others. An implementation of our algorithm beats solvers for more general probabilistic hyperlogics by orders of magnitude, on the subset of their benchmarks that are within our fragment.

Reward shaping in multi-agent reinforcement learning (MARL) for complex tasks remains a significant challenge. Existing approaches often fail to find optimal solutions or cannot efficiently handle such tasks. We propose HypRL, a specification-guided reinforcement learning framework that learns control policies w.r.t. hyperproperties expressed in HyperLTL. Hyperproperties constitute a powerful formalism for specifying objectives and constraints over sets of execution traces across agents. To learn policies that maximize the satisfaction of a HyperLTL formula $\varphi$, we apply Skolemization to manage quantifier alternations and define quantitative robustness functions to shape rewards over execution traces of a Markov decision process with unknown transitions. A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward and, consequently, increase the probability of satisfying $\varphi$. We evaluate HypRL on a diverse set of benchmarks, including safety-aware planning, Deep Sea Treasure, and the Post Correspondence Problem. We also compare with specification-driven baselines to demonstrate the effectiveness and efficiency of HypRL.

Abstract Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.

Abstract We study the problem of automatically repairing infinite-state software programs w.r.t. temporal hyperproperties. As a first step, we present a repair approach for the temporal logic HyperLTL based on symbolic execution, constraint generation, and syntax-guided synthesis of repair expression (SyGuS). To improve the repair quality, we introduce the notation of a transparent repair that aims to find a patch that is as close as possible to the original program. As a practical realization, we develop an iterative repair approach. Here, we search for a sequence of repairs that are closer and closer to the original program’s behavior. We implement our method in a prototype and report on encouraging experimental results using off-the-shelf SyGuS solvers.

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.

Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on the cause. In this article, we propose a novel and effective method to formally reason about the causal effect of events in engineered systems, with application for finding the root-cause of safety violations in embedded and cyber-physical systems. We are motivated by the notion of actual causality by Halpern and Pearl, which focuses on the causal effect of particular events rather than type-level causality, which attempts to make general statements about scientific and natural phenomena. Our first contribution is formulating discovery of actual causality in computing systems modeled by transition systems as an satisfiability modulo theory solving problem. Since datasets for causality analysis tend to be large, in order to tackle the scalability problem of automated formal reasoning, our second contribution is a novel technique based on abstraction refinement that allows identifying for actual causes within smaller abstract causal models. We demonstrate the effectiveness of our approach (by several orders of magnitude) using three case studies to find the actual cause of violations of safety in 1) a neural network controller for a mountain car; 2) a controller for a Lunar Lander obtained by reinforcement learning; and 3) an MPC controller for an F-16 autopilot simulator.

Runtime verificationis a technique, where amonitorprocess extracts information from a running system in order to evaluate whether system executions violate or satisfy a given correctness specification. In this paper, we consider runtime verification of synchronous distributed systems, where a set of decentralized monitors that only have a partial view of the system are subject tocrash failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and, therefore, have different opinions about the correctness property. We propose an automata-based synchronous monitoring algorithm that copes with$t$crash monitor failures. In our proposed approach, local monitors do not communicate their explicit reading of the underlying system. Rather, they emit asymbolic verdictthat efficiently encodes their partial views. This significantly reduces the communication overhead. To this end, we also introduce an (offline) SMT-based monitor synthesis algorithm, which results in minimizing the size of monitoring messages. We evaluate our algorithm on a wide range of formulas and observe an average of 2.5 times increase in the number of states of the monitor automaton.

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.

Abstract Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in. We focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties . We generalize the temporal logic to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for based on QBF-solving for a fragment of and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking .

Abstract Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on developing loop conditions for BMC of – a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for are more complicated than for , as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for BMC, for formulas that contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using .

In system design, high-level system models typically need to be mapped to an execution platform (e.g., hardware, environment, compiler, etc). The platform may naturally strengthen some constraints or weaken some others, but it is expected that the low-level implementation on the platform should preserve all the functional and extra-functional properties of the model, including the ones for information-flow security. It is, however, well known that simple notions of refinement do not preserve information-flow security properties. In this paper, we propose a novel automated mapping synthesis approach that preserves hyperproperties expressed in the temporal logic HyperLTL. The significance of our technique is that it can handle formulas with quantifier alternations, which is typically the source of difficulty in refinement for information-flow security policies. We reduce the mapping synthesis problem to HyperLTL model checking and leverage recent efforts in bounded model checking for hyperproperties. We demonstrate how mapping synthesis can be used in various applications, including enforcing non-interference and automating secrecy-preserving refinement mapping. We also evaluate our approach using the battleship game and password validation use cases.

Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Verifying the runtime correctness of smart contracts is a problem of compelling practical interest since, smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties. Such verification is challenging since smart contract execution is time sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring MTL specifications which employs SMT solving techniques and report experimental results.

Abstract Randomization is a key concept in distributed computing to tackle impossibility results. This also holds for self-stabilization in anonymous networks where coin flips are often used to break symmetry. Although the use of randomization in self-stabilizing algorithms is rather common, it is unclear what the optimal coin bias is so as to minimize the expected convergence time. This paper proposes a technique to automatically synthesize this optimal coin bias. Our algorithm is based on a parameter synthesis approach from the field of probabilistic model checking. It over- and under-approximates a given parameter region and iteratively refines the regions with minimal convergence time up to the desired accuracy. We describe the technique in detail and present a simple parallelization that gives an almost linear speed-up. We show the applicability of our technique to determine the optimal bias for the well-known Herman’s self-stabilizing token ring algorithm. Our synthesis obtains that for small rings, a fair coin is optimal, whereas for larger rings a biased coin is optimal where the bias grows with the ring size. We also analyze a variant of Herman’s algorithm that coincides with the original algorithm but deviates for biased coins. Finally, we show how using speed reducers in Herman’s protocol improve the expected convergence time.

Runtime verification is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors observing the system, only if each monitor can emit verdicts taken from a large enough finite set. We revisit this impossibility result in the concrete context of linear-time logic ( ltl ) semantics for runtime verification, that is, when the correctness of the system is specified by an ltl formula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics of ltl ( rv-ltl ) may result in inconsistent distributed monitoring, even for some simple ltl formulas. More generally, given any ltl formula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called its alternation number . Specifically, we show that, for every k ≥ 0 , there is an ltl formula φ with alternation number k that cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller than k + 1. On the positive side, we define a family of logics, called distributed ltl (abbreviated as dltl ), parameterized by k ≥ 0, which refines rv-ltl by incorporating 2k + 4 truth values. Our main contribution is to show that, for every k ≥ 0, every ltl formula φ with alternation number k can be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈ k /2 ⌉ +4)-valued logic taken from the dltl family.

Abstract Hyperpropertiesare properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics aresynchronousin the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose anasynchronousvariant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.

Hyperproperties have shown to be a powerful tool for expressing and reasoning about information-flow security policies. In this paper, we investigate the problem of statistical model checking (SMC) for hyperproperties. Unlike exhaustive model checking, SMC works based on drawing samples from the system at hand and evaluate the specification with statistical confidence. The main benefit of applying SMC over exhaustive techniques is its efficiency and scalability. To reason about probabilistic hyperproperties, we first propose the temporal logic HyperPCTL* that extends PCTL* and HyperPCTL. We show that HyperPCTL* can express important probabilistic information-flow security policies that cannot be expressed with HyperPCTL. Then, we introduce SMC algorithms for verifying HyperPCTL* formulas on discrete-time Markov chains, based on sequential probability ratio tests (SPRT) with a new notion of multidimensional indifference region. Our SMC algorithms can handle both non-nested and nested probability operators for any desired significance level. To show the effectiveness of our technique, we evaluate our SMC algorithms on four case studies focused on information security: timing side-channel vulnerability in encryption, probabilistic anonymity in dining cryptographers, probabilistic noninterference of parallel programs, and the performance of a randomized cache replacement policy that acts as a countermeasure against cache flush attacks.

In this paper, we propose an approach to extend the operational time of teams of battery-based robots by introducing a set of charging stations. We assume that the robots are heterogeneous (having different energy limits and being able to service different types of customers) and have access to a priori known map of the environment. The map is modeled as a directed, connected, and finite graph whose nodes are charging stations or customers, and arcs denote the possibility of traveling. To this end, we first formulate a task assignment and path planning problem that aims at optimizing energy consumption as well as the time needed to complete the tasks, including the time spent for recharging. Next, we propose four offline optimization techniques and one online algorithm, where the robots can dynamically adjust their paths in response to the presence of uncertainties imposed by the physical environment. Our proposed algorithms are validated through both simulation and a real-world case study on a team of unmanned aerial vehicles (UAVs) performing a joint search mission.

In this paper, we propose an automated technique for synthesizing fault-tolerant distributed protocols from their fault-intolerant version, where the number of processes is parameterized. A fault-tolerant protocol is one that ensures constant satisfaction of safety and liveness specifications even in the presence of faults. Although the parametrized synthesis problem is undecidable in general, we could propose a sound algorithm for this challenging problem. Our synthesis algorithm utilizes counter abstraction to construct a finite representation of the state space. Then, it performs fixpoint calculations to compute and exclude states that violate the safety/liveness specifications in the presence of faults. We demonstrate the effectiveness of our algorithm by synthesizing fault-tolerant distributed protocols for well-known problems, such as reliable broadcast and a simplified version of Byzantine agreement in a matter of seconds.

Abstract This paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which — to the best of our knowledge — is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. Our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. We report on successful and efficient model checking, implemented in our tool called , of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and mutation testing.

Abstract Runtime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both for trace properties and hyperproperties, taking into account, among other things, the computability of the monitor. A second contribution of our work is to show that black-box monitoring of HyperLTL (a logic for hyperproperties) is in general unfeasible, and to suggest a gray-box approach in which we combine static and runtime verification. The main idea is to call a static verifier as an oracle at run time allowing, in some cases, to give a final verdict for properties that are considered to be non-monitorable under a black-box approach. Our third contribution is the instantiation of this solution to a privacy property called distributed data minimization which cannot be verified using black-box runtime verification. We use an SMT-based static verifier as an oracle at run time. We have implemented our gray-box approach for monitoring data minimization into the proof-of-concept tool Minion. We describe the tool and apply it to a few case studies to show its feasibility.

We investigate the problem of controller synthesis for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple execution traces. Hyperproperties can elegantly express information-flow policies like noninterference and observational determinism. The controller synthesis problem is to automatically design a controller for a plant that ensures satisfaction of a given specification in the presence of the environment or adversarial actions. We show that the controller synthesis problem is decidable for HyperLTL specifications and finite-state plants. We provide a rigorous complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general graphs.

In this paper, we study the parameter synthesis problem for probabilistic hyperproper- ties. A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. In particular, we solve the following problem: given a probabilistic hyperprop- erty ψ and discrete-time Markov chain D with parametric transition probabilities, compute regions of parameter configurations that instantiate D to satisfy ψ, and regions that lead to violation. We address this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.

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.

The first international Competition on Runtime Verification (CRV) was held in September 2014, in Toronto, Canada, as a satellite event of the 14th international conference on Runtime Verification (RV’14). The event was organized in three tracks: (1) offline monitoring, (2) online monitoring of C programs, and (3) online monitoring of Java programs. In this paper, we report on the phases and rules, a description of the participating teams and their submitted benchmark, the (full) results, as well as the lessons learned from the competition.

Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabilistic fairness and sensitivity to modeling errors (i.e., parameters changes) for real-valued signals. These requirements can only be specified by hyperproperties . In this article, we focus on verifying probabilistic hyperproperties for CPS. To cover a wide range of modeling formalisms, we first propose a general model of probabilistic uncertain systems (PUSs) that unify commonly studied CPS models such as continuous-time Markov chains (CTMCs) and probabilistically parametrized Hybrid I/O Automata (P 2 HIOA). To formally specify hyperproperties, we propose a new temporal logic, hyper probabilistic signal temporal logic (HyperPSTL) that serves as a hyper and probabilistic version of the conventional signal temporal logic (STL). Considering the complexity of real-world systems that can be captured as PUSs, we adopt a statistical model checking (SMC) approach for their verification. We develop a new SMC technique based on the direct computation of significance levels of statistical assertions for HyperPSTL specifications, which requires no a priori knowledge on the indifference margin. Then, we introduce SMC algorithms for HyperPSTL specifications on the joint probabilistic distribution of multiple paths, as well as specifications with nested probabilistic operators quantifying different paths, which cannot be handled by existing SMC algorithms. Finally, we show the effectiveness of our SMC algorithms on CPS benchmarks with varying levels of complexity, including the Toyota Powertrain Control System.

Hardware energy efficiency has been one of the prominent objectives of system design in the last two decades. However, with the recent explosion in mobile computing and the increasing demand for green data centers, software energy efficiency has also risen to be an equally important factor. The majority of classic concurrency control algorithms were designed in an era when energy efficiency was not an important dimension in algorithm design. Concurrency control algorithms are applied to solve a wide range of problems from kernel-level primitives in operating systems to networking devices and web services. These primitives and services are constantly and heavily invoked in any computing system and by a larger scale in networking devices and data centers. Thus, even a small change in their energy spectrum can make a huge impact on overall energy consumption for long periods of time. This paper focuses on the classic producer-consumer problem. First, we study the energy profile of a set of existing producer-consumer algorithms. In particular, we present evidence that although these algorithms share the same functional goals, their behavior with respect to energy consumption are drastically different. Then, we present a dynamic algorithm for the multiple producer-consumer problem, where consumers in a multicore system use learning mechanisms to predict the rate of production, and effectively utilize this prediction to attempt to latch onto previously scheduled CPU wake-ups. Such group latching increases the idle time between consumer activations resulting in more CPU idle time and, hence, lower average CPU frequency. This in turn reduces energy consumption. We enable consumers to dynamically reserve more pre-allocated memory in cases where the production rate is too high. Consumers may compete for the extra space and dynamically release it when it is no longer needed. Our experiments show that our algorithm provides a 38 percent decrease in energy consumption compared to a mainstream semaphore-based producer-consumer implementation when running 10 parallel consumers. We validate the effectiveness of our algorithm with a set of thorough experiments on varying parameters of scalability. Finally, we present our recommendations on when our algorithm is most beneficial.

We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors for hyperproperties analyze trace logs that are organized by common prefixes in the form of a tree-shaped Kripke structure, or are organized both by common prefixes and by common suffixes in the form of an acyclic Kripke structure. Unlike runtime verification techniques for trace properties, where the monitor tracks the state of the specification but usually does not need to store traces, a monitor for hyperproperties repeatedly model checks the growing Kripke structure. This calls for a rigorous complexity analysis of the model checking problem over tree-shaped and acyclic Kripke structures. We show that for trees, the complexity in the size of the Kripke structure is L-complete independently of the number of quantifier alternations in the HyperLTL formula. For acyclic Kripke structures, the complexity is PSPACE-complete (in the level of the polynomial hierarchy that corresponds to the number of quantifier alternations). The combined complexity in the size of the Kripke structure and the length of the HyperLTL formula is PSPACE-complete for both trees and acyclic Kripke structures, and is as low as NC for the relevant case of trees and alternation-free HyperLTL formulas. Thus, the size and shape of both the Kripke structure and the formula have significant impact on the complexity of the model checking problem.

Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.

In this paper, we consider runtime verification of synchronous distributed systems, where a decentralized set of monitors that only have a partial view of the system are subject to crash failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and, therefore, have different opinions about the correctness property. We propose an automata-based synchronous monitoring algorithm that copes with t crash monitor failures. Moreover, local monitors do not communicate their explicit reading of the underlying system. Rather, they emit a symbolic verdict that efficiently encodes their partial views. This significantly reduces the communication overhead.

In this article, we focus on efficient synthesis of fault-tolerant timed models from their fault-intolerant version. Although the complexity of the synthesis problem is known to be polynomial time in the size of the time-abstract bisimulation of the input model, the state of the art currently lacks synthesis algorithms that can be efficiently implemented. This is in part due to the fact that synthesis is in general a challenging problem and its complexity is significantly magnified in the context of timed systems. We propose an algorithm that takes as input a timed automaton, a set of fault actions, and a set of safety and bounded-time response properties, and utilizes a space-efficient symbolic representation of the timed automaton (called zone graph) to synthesize a fault-tolerant timed automaton as output. The output automaton satisfies strict phased recovery, where it is guaranteed that the output model behaves similarly to the input model in the absence of faults and in the presence of faults, fault recovery is achieved in two phases, each satisfying certain safety and timing constraints.

The classic vehicle routing problem (VRP) is generally concerned with the optimal design of routes by a fleet of vehicles to service a set of customers by minimizing the overall cost, usually the travel distance for the whole set of routes. Although the problem has been extensively studied in the context of operations research and optimization, there is little research on solving the VRP, where distributed vehicles need to compute their respective routes in a decentralized fashion. Our first contribution is a synchronous distributed approximation algorithm that solves the VRP. Using the duality theorem of linear programming, we show that the approximation ratio of our algorithm is O(n · (ρ)1/nlog(n + m)), where ρ is the maximum cost of travel or service in the input VRP instance, n is the size of the graph, and m is the number of vehicles. We report results of simulations and discuss implementation of our algorithm on a real fleet of unmanned aerial systems (UASs) that carry out a set of tasks.

Although randomized algorithms have widely been used in distributed computing as a means to tackle impossibility results, it is currently unclear what type of randomization leads to the best performance in such algorithms. This paper proposes three automated techniques to find the probability distribution that achieves minimum average recovery time for an input randomized distributed self-stabilizing protocol without changing the behavior of the algorithm. Our first technique is based on solving symbolic linear algebraic equations in order to identify fastest state reachability in parametric discrete-time Markov chains. The second approach applies parameter synthesis techniques from probabilistic model checking to compute the rational function describing the average recovery time and then uses dedicated solvers to find the optimal parameter valuation. The third approach computes over- and under-approximations of the result for a given parameter region and iteratively refines the regions with minimal recovery time up to the desired precision. The latter approach finds sub-optimal solutions with negligible errors, but it is significantly more scalable in orders of magnitude as compared to the other approaches.

Modern embedded systems are becoming more reliant on real-valued arithmetic as they employ mathematically complex vision algorithms and sensor signal processing. Double-precision floating point is the most commonly used precision in computer vision algorithm implementations. A single-precision floating point can provide a performance boost due to less memory transfers, less cache occupancy, and relatively faster mathematical operations on some architectures. However, adopting it can result in loss of accuracy. Identifying which parts of the program can run in single-precision floating point with low impact on error is a manual and tedious process. In this paper, we propose an automatic approach to identify parts of the program that have a low impact on error using shadow-value analysis. Our approach provides the user with a performance/error tradeoff, using which the user can decide how much accuracy can be sacrificed in return for performance improvement. We illustrate the impact of the approach using a well known implementation of Apriltag detection used in robotics vision. We demonstrate that an average 1.3x speedup can be achieved with no impact on tag detection, and a 1.7x speedup with only 4% false negatives.

This paper introduces a novel runtime verification technique for a rich sub-class of Clarkson and Schneider's hyperproperties. The primary application of such properties is in expressing security policies (e.g., information flow) that cannot be expressed in trace-based specification languages (e.g., LTL). First, to incorporate syntactic means, we draw connections between safety and co-safety hyperproperties and the temporal logic HYPERLTL, which allows explicit quantification over multiple executions. We also define the notion of monitorability in HYPERLTL and identify classes of monitorable HYPERLTL formulas. Then, we introduce an algorithm for monitoring k-safety and co-k-safety hyperproperties expressed in HYPERLTL. Our technique is based on runtime formula progression as well as on-the-fly monitor synthesis across multiple executions. We analyze different performance aspects of our technique by conducting thorough experiments on monitoring security policies for information flow and observational determinism on a real-world location-based service dataset as well as synthetic trace sets.

Automata-based models of embedded systems are useful and attractive for many reasons: they are intuitive, precise, at a high level of abstraction, tool independent and can be simulated and analyzed. They also have the advantage of facilitating readability and system comprehension in the case of large systems. This paper proposes an approach for mining automata-based models from input/output execution traces of embedded control systems. The models mined by our approach are hybrid automata models, which capture discrete as well as continuous system behavior. Specifically this paper proposes a framework for analyzing multiple input/output traces by identifying steps like segmentation, clustering, generation of event traces, and automata inference. The framework is general enough to admit multiple techniques or future enhancements of these steps. We demonstrate the power of the framework by using some specific existing methods and tools in two case studies. Our initial results are encouraging and should spur further research in the domain.

A self-stabilizing system is one that converges to a legitimate state from any arbitrary state. Such an arbitrary state may be reachable due to wrong initialization or the occurrence of transient faults. Average recovery time of self-stabilizing systems is a key factor in evaluating their performance, especially in the domain of network and robotic protocols. This paper introduces a groundbreaking result on automated repair and synthesis of self-stabilizing protocols whose average recovery time is required to satisfy certain constraints. We show that synthesizing and repairing weak-stabilizing protocols under average recovery time constraints is NP-complete. To cope with the exponential complexity (unless P = NP), we propose a polynomial-time heuristic.

Runtime verification is a lightweight automated formal method for specification-based runtime monitoring as well as testing of large real-world systems. While numerous techniques exist for runtime verification of sequential programs, there has been very little work on specification-based monitoring of distributed systems. In this paper, we propose the first sound and complete method for runtime verification of asynchronous distributed programs for the 3-valued semantics of LTL specifications defined over the global state of the program. Our technique for evaluating LTL properties is inspired by distributed computation slicing, an approach for abstracting distributed computations with respect to a given predicate. Our monitoring technique is fully decentralized in that each process in the distributed program under inspection maintains a replica of the monitor automaton. Each monitor may maintain a set of possible verification verdicts based upon existence of concurrent events. Our experiments on runtime monitoring of a simulated swarm of flying drones show that due to the design of our Algorithm, monitoring overhead grows only in the linear order of the number of processes and events that need to be monitored.

Abstract We focus on synthesis techniques for transforming existing fault-intolerant real-time programs into fault-tolerant programs that provide phased recovery . A fault-tolerant program is one that satisfies its safety and liveness specifications as well as timing constraints in the presence of faults. We argue that in many commonly considered programs (especially in safety/mission-critical systems), when faults occur, simple recovery to the program’s normal behavior is necessary, but not sufficient. For such programs, it is necessary that recovery is accomplished in a sequence of phases, each ensuring that the program satisfies certain properties. In the simplest case, in the first phase the program recovers to an acceptable behavior within some time θ , and, in the second phase, it recovers to the ideal behavior within time δ . In this article, we introduce four different types of bounded-time 2-phase recovery, namely ordered-strict, strict, relaxed, and graceful, based on how a real-time fault-tolerant program reaches the acceptable and ideal behaviors in the presence of faults. We rigorously analyze the complexity of automated synthesis of each type: we either show that the problem is hard in some class of complexity or we present a sound and complete synthesis algorithm. We argue that such complexity analysis is essential to deal with the highly complex decision procedures of program synthesis.

A self-stabilizing system is one that guarantees reaching a set of legitimate states from any arbitrary initial state. Designing distributed self-stabilizing protocols is often a complex task and developing their proof of correctness is known to be significantly more tedious. In this article, we propose an SMT-based method that automatically synthesizes a self-stabilizing protocol, given the network topology of distributed processes and description of the set of legitimate states. Our method can synthesize synchronous, asynchronous, symmetric, and asymmetric protocols for two types of stabilization, namely weak and strong . We also report on successful automated synthesis of a set of well-known distributed stabilizing protocols such as Dijkstra’s token ring, distributed maximal matching, graph coloring, and mutual exclusion in anonymous networks.

The goal of runtime monitoring is to inspect the well-being of a system by employing a monitor process that reads the state of the system during execution and evaluates a set of properties expressed in some specification language. The main challenge in runtime monitoring is dealing with the costs imposed in terms of resource utilization. In the context of cyber-physical systems, it is crucial for a software monitoring solution to be time predictable to improve scheduling, as well as support composition of monitoring solutions with an overall predictable behavior. Moreover, a small memory footprint is often required in components of cyber-physical systems, especially in deeply embedded systems. In this article, we propose a novel control-theoretic software monitoring solution for coordinating time predictability and memory utilization in runtime monitoring of systems that interact with the physical world. The controllers attempt to reduce monitoring jitter and maximize memory utilization while simultaneously ensuring the soundness of evaluation of properties. For systems where multiple properties are required to be monitored simultaneously, we construct a buffer sharing mechanism in which controllers dynamically share the memory space to negate the effect of bursts of environment actions, thus reducing jitter due to transient high loads. To validate our design choices, we present three case studies: (1) a Bluetooth mobile payment system, which shows a sporadic rate of events during peak hours; (2) a laser beam stabilizer for target tracking, and (3) a monitoring system for air/fuel ratio in a car engine exhaust and the CAM inlet position in the engine’s cylinders. The experimental results of the case studies demonstrate up to 40% improvement in time predictability of the monitoring solution when compared to a basic event-triggered approach. Moreover, memory utilization reaches an average of 90% when using our dynamic buffer resizing mechanism.

Power efficiency has been one of the main objectives of hardware design in the last two decades. However, with the recent explosion of mobile computing and the increasing demand for green data centers, software power efficiency has also risen to be an equally important factor. We argue that most classic concurrency control algorithms were designed in an era when power efficiency was not an important dimension in algorithm design. Such algorithms are applied to solve a wide range of problems from kernel-level primitives in operating systems to networking devices and web services. These primitives and services are constantly and heavily invoked in any computer system and by larger scale in networking devices and data centers. Thus, even a small change in their power spectrum can make a huge impact on overall power consumption in long periods of time. This paper focuses on the classic producer-consumer problem. First, we study the power efficiency of different existing implementations of the producer-consumer problem. In particular, we present evidence that these implementations behave drastically differently with respect to power consumption. Secondly, we present a dynamic algorithm for the multiple producer-consumer problem, where consumers in a multicore system use learning mechanisms to predict the rate of production, and effectively utilize this prediction to attempt to latch onto previously scheduled CPU wake-ups. Such group latching results in minimizing the overall number of CPU wakeups and in effect, power consumption. We enable consumers to dynamically reserve more pre-allocated memory in cases where the production rate is too high. Consumers may compete for the extra space and dynamically release it when it is no longer needed. Our experiments show that our algorithm provides up to 40% decrease in the number of CPU wakeups, and 30% decrease in power consumption. We validate the scalability of our algorithm with an increasing number of consumers.

Runtime verification is a monitoring technique to gain assurance about well-being of a program at run time. Most existing approaches use sequential monitors; i.e., when the state of the program with respect to an event of interest changes, the monitor interrupts the program execution, evaluates a set of logical properties, and finally resumes the program execution. In this paper, we propose a GPU-based method for design and implementation of monitors that enjoy two levels of parallelism: the monitor (1) works along with the program in parallel, and (2) evaluates a set of properties in a parallel fashion as well. Our parallel monitoring algorithms effectively exploit the many-core platform available in the GPU. In addition to parallel processing, our approach benefits from a true separation of monitoring and functional concerns, as it isolates the monitor in the GPU. Our method is fully implemented and experimental results show significant reduction in monitoring overhead, monitoring interference, and power consumption due to leveraging the GPU technology.

We introduce the tool RiTHM (Runtime Time-triggered Heterogeneous Monitoring). RiTHM takes a C program under inspection and a set of LTL properties as input and generates an instrumented C program that is verified at run time by a time-triggered monitor. RiTHM provides two techniques based on static analysis and control theory to minimize instrumentation of the input C program and monitoring intervention. The monitor's verification decision procedure is sound and complete and exploits the GPU many-core technology to speedup and encapsulate monitoring tasks.

We propose a new metric for effectively and accurately evaluating the performance of self-stabilizing algorithms. Self-stabilization is a versatile category of fault-tolerance that guarantees system recovery to normal behavior within a finite number of steps, when the state of the system is perturbed by transient faults (or equally, the initial state of the system can be some arbitrary state). The performance of self-stabilizing algorithms is conventionally characterized in the literature by asymptotic computation complexity. We argue that such characterization of performance is too abstract and does not reflect accurately the realities of deploying a distributed algorithm in practice. Our new metric for characterizing the performance of self-stabilizing algorithms is the expected mean value of recovery time. Our metric has several crucial features. Firstly, it encodes accurate average case speed of recovery. Secondly, we show that our evaluation method can effectively incorporate several other parameters that are of importance in practice and have no place in asymptotic computation complexity. Examples include the type of distributed scheduler, likelihood of occurrence of faults, the impact of faults on speed of recovery, and network topology. We utilize a deep analysis technique, namely, probabilistic model checking to rigorously compute our proposed metric. All our claims are backed by detailed case studies and experiments.

Time-triggered runtime verification aims at tackling two defects associated with runtime overhead: unboundedness and unpredictability. In this approach, a monitor runs in parallel with the program under inspection and periodically samples the program state to evaluate a set of properties. The fact that the monitoring tasks place only at predictable time ticks makes the approach predictable and especially suitable for embedded systems.

Runtime monitoring aims at analyzing the well-being of a system at run time in order to detect errors and steer the system towards a healthy behavior. Such monitoring is a complementary technique to other approaches for ensuring correctness, such as formal verification and testing. In time-triggered runtime monitoring, a monitor runs as a separate process in parallel with an application program under scrutiny and samples the program's state periodically to evaluate a set of properties. Applying this technique in a computing system results in obtaining bounded and predictable overhead. Gaining such characteristics for overhead is highly desirable for designing and engineering time-critical applications, such as safety-critical embedded systems. However, a time-triggered monitor requires certain synchronization features at operating system level and may suffer from various concurrency and synchronization dependencies and overheads as well as possible unreliability of synchronization primitives in a real-time setting. In this paper, we propose a new method, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or internal timer. We call this technique time-triggered self-monitoring. First, we formulate an optimization problem for minimizing the number of points in a program, where self-sampling instrumentation instructions must be inserted. We show that this problem is NP-complete. Consequently, we propose a SAT-based solution and a heuristic to cope with the exponential complexity. Our experimental results show that a time-triggered self-monitored program performs significantly better than the same program monitored by an external time-triggered monitor.

In this paper, we introduce a novel model-based approach for constructing correct distributed implementation of component-based models constrained by priorities. We argue that model-based methods are especially of interest in the context of distributed embedded system due to their inherent complexity. Our three-phase method's input is a model specified in terms of a set of behavioural components that interact through a set of high-level synchronization primitives (e.g., rendezvous and broadcasts) and priority rules for scheduling purposes. Our technique, first, transforms the input model into a model that has no priorities. Then, it transforms the deprioritized model into another model that resolves distributed conflicts by incorporating a solution to the committee coordination problem. Finally, it generates distributed code using asynchronous point-to-point send/receive primitives. All transformations preserve the properties of their input model by ensuring observational equivalence. The transformations are implemented and our experiments validate their effectiveness.

In this paper, we concentrate on automated synthesis of fault recovery mechanism for fault-intolerant component-based models that encompass a cyber-physical system. We define the notion of fault recovery for cyber-physical component-based models. We also present synthesis constraints that preserve the correctness and cyber-physical nature of a given fault-intolerant model under which recovery can be added. We show that the corresponding synthesis problem is NP-complete and consequently introduce symbolic heuristics to tackle the exponential complexity. Our experimental results validate effectiveness of our heuristics for relatively large models.

In this paper, we propose two snap-stabilizing distributed algorithms for the committee coordination problem. In this problem, a committee consists of a set of processes and committee meetings are synchronized, so that each process participates in at most one committee meeting at a time. Snap-stabilization is a versatile technique allowing to design algorithms that efficiently tolerate transient faults. Indeed, after a finite number of such faults (e.g. memory corruptions, message losses, etc), a snap-stabilizing algorithm immediately operates correctly, without any external intervention. We design snap-stabilizing committee coordination algorithms enriched with some desirable properties related to concurrency, (weak) fairness, and a stronger synchronization mechanism called 2-Phase Discussion Time. From previous papers, we know that (1) in the general case, (weak) fairness cannot be achieved in the committee coordination, and (2) it becomes feasible provided that each process waits for meetings infinitely often. Nevertheless, we show that even under this latter assumption, it is impossible to implement a fair solution that allows maximal concurrency. Hence, we propose two orthogonal snap-stabilizing algorithms, each satisfying 2-phase discussion time, and either maximal concurrency or fairness. The algorithm implementing fairness requires that every process waits for meetings infinitely often. Moreover, for this algorithm, we introduce and evaluate a new efficiency criterion called the degree of fair concurrency. This criterion shows that even if it does not satisfy maximal concurrency, our snap-stabilizing fair algorithm still allows a high level of concurrency.

In this paper, we present a notion of observability and controllability in the context of software testing and debugging. Our view of observability is based on the ability of developers, testers, and debuggers to trace back a data dependency chain and observe the value of a variable by starting from a set of variables that are naturally observable (e.g., input/output variables). Likewise, our view of controllability enables one to modify and control the value of a variable through a data dependency chain by starting from a set of variables that can be modified (e.g., input variables). Consequently, the problem that we study in this paper is to identify the minimum number of variables that have to be made observable/controllable in order for a tester or debugger to observe/control the value of another set of variables of interest, given the source code. We show that our problem is an instance of the well-known abstract diagnosis problem, where the objective is to find the minimum number of faulty components in a digital circuit, given the system description and value of input/output variables. We show that our problem is NP-complete even if the length of data dependencies is at most 2. In order to cope with the inevitable exponential complexity, we propose a mapping from the general problem, where the length of data dependency chains is unknown a priori, to integer linear programming. Our method is fully implemented in a tool chain for MISRA-C compliant source codes. Our experiments with several real-world applications show that in average, a significant number of debugging points can be reduced using our methods. This result is our motivation to apply our approach in debugging and instrumentation of embedded software, where changes must be minimal as they can perturb the timing constraints and resource consumption. Another interesting application of our results is in data logging of non-terminating embedded systems, where axillary data storage devices are slow and have limited size.

This paper introduces a theory of fault recovery for component-based models. In our framework, a model is specified in terms of a set of atomic components that are incrementally composed and synchronized by a set of glue operators. We define what it means for such models to provide a recovery mechanism, so that the model converges to its normal behavior in the presence of faults. We identify corrector (atomic or composite) components whose presence in a model is essential to guarantee recovery after the occurrence of faults. We also formalize component-based models that effectively separate recovery from functional concerns.

Although distributed systems are widely used nowadays, their implementation and deployment is still a time-consuming, error-prone, and hardly predictive task. In this paper, we propose a methodology for producing automatically efficient and correct-by-construction distributed implementations by starting from a high-level model of the application software in BIP. BIP (Behavior, Interaction, Priority) is a component-based framework with formal semantics that rely on multi-party interactions for synchronizing components. Our methodology transforms arbitrary BIP models into Send/Receive BIP models, directly implementable on distributed execution platforms. The transformation consists of (1) breaking atomicity of actions in atomic components by replacing strong synchronizations with asynchronous Send/Receive interactions; (2) inserting several distributed controllers that coordinate execution of interactions according to a user-defined partition, and (3) augmenting the model with a distributed algorithm for handling conflicts between controllers preserving observational equivalence to the initial models. Currently, it is possible to generate from Send/Receive models stand-alone C++ implementations using either TCP sockets for conventional communication, or MPI implementation, for deployment on multi-core platforms. This method is fully implemented. We report concrete results obtained under different scenarios.

A hard-masking real-time program is one that satisfies safety (including timing constraints) and liveness properties in the absence and presence of faults. It has been shown that any hard-masking program can be decomposed into a fault-intolerant version and a set of fault-tolerance components known as detectors and delta-correctors. In this paper, we introduce a set of sufficient conditions for interference-freedom among fault-tolerance components and real-time programs. We demonstrate that such conditions elegantly enable us to compositionally verify the correctness of hard-masking programs. Preliminary model checking experiments show very encouraging results in both achieving speedups and reducing memory usage in verification of embedded systems.

We concentrate on automatic revision of untimed and real-time programs with respect to UNITY properties. The main focus of this article is to identify instances where addition of UNITY properties can be achieved efficiently (in polynomial time) and where the problem of adding UNITY properties is difficult (NP-complete). Regarding efficient revision, we present a sound and complete algorithm that adds a singleleads-toproperty (respectively,bounded-time leads-toproperty) and a conjunction ofunless, stable, andinvariantproperties (respectively,bounded-time unlessandstable) to an existing untimed (respectively, real-time) UNITY program in polynomial-time in the state space (respectively, region graph) of the given program. Regarding hardness results, we show that (1) while oneleads-to(respectively,ensures) property can be added in polynomial-time, the problem of adding two such properties (or any combination ofleads-toandensures) is NP-complete, (2) if maximum non-determinism is desired then the problem of adding even a singleleads-toproperty is NP-complete, and (3) the problem of providing maximum non-determinism while adding a singlebounded-time leads-toproperty to a real-time program is NP-complete (in the size of the program's region graph) even if the original program satisfies the correspondingunbounded leads-toproperty.

We focus on decomposition of hard-masking real-time fault-tolerant programs (where safety, timing constraints, and liveness are preserved in the presence of faults) that are designed from their fault-intolerant versions. Towards this end, motivated by the concepts of state predicate detection and state predicate correction, we identify three types of fault-tolerance components, namely, detectors, weak S-correctors, and strong S-correctors. We show that any hard-masking program can be decomposed into its fault-intolerant version plus a collection of detectors, and, weak and strong S-correctors. We argue that such decomposition assists in providing assurance about dependability and time-predictability of embedded systems.

Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time complexity of their decision procedures and also high space complexity known as the state explosion problem. Symbolic techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy the state explosion problem and time complexity of decision procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond 2100) is handled during synthesis.