Falsification testing is a popular method for efficiently identifying inputs that witness the violation of cyber-physical system (CPS) specifications. The generated counterexamples are used to locate and explain faults and debug the system. However, CPS rarely operate in unconstrained environments and not all counterexamples have the same value. On one hand, faults resulting from common system usage are more likely to happen in practice than faults triggered by esoteric inputs. On the other hand, some faults can have more severe consequences than others. Together, the probability and the severity of a fault determine its risk, an important aspect that is neglected by the existing falsification testing techniques. We propose a new falsification testing methodology that is aware of the system’s expected usage and the severity associated to different faulty behaviors. Given a user profile in the form of a stochastic hybrid automaton, an associated severity degree measure, an executable black-box implementation of the CPS and its formalized requirements, we provide a test generation method that (1) uses efficient randomized methods to generate multiple violating traces, and (2) estimates the probability and the expected severity, and hence the expected risk of each counterexample, thus providing their ranking to the engineer.
Cyber-physical systems often require fault detection of future events in order to mitigate the fault before failure occurs. Effective on-board runtime verification (RV) will need to not only determine the system’s current state but also predict future faults by predetermined mitigation trigger deadlines. For example, if it takes three seconds to deploy the parachute of an Unmanned Aerial System (UAS), the deployment of the parachute must be triggered three seconds before it is needed to mitigate the impending crash. To allow for the detection of future faults by deadlines, we design a real-time Model Predictive Runtime Verification (MPRV) algorithm that uniquely uses current data traces whenever possible, predicting only the minimum horizon needed to make an on-deadline evaluation. Although MPRV is extensible to other RV engines, we deploy the algorithm on the R2U2 RV engine due to R2U2’s resource-aware architecture, real-time guarantees, and deployment history. We demonstrate the utility of the MPRV algorithm through a quadcopter case study and evaluate the effectiveness of our implementation by conducting memory usage and runtime performance analysis in a resource-constrained FPGA environment.
Mission-time Linear Temporal Logic (MLTL) is a variant of Linear Temporal Logic (LTL) with finite interval bounds on temporal operators, and is a popular formal specification language for safety-critical cyber-physical systems. Given a set of specifications, the maximum satisfiability problem (MaxSAT) asks to find the maximum number of simultaneously satisfiable specifications. MaxSAT is useful for system designing complex systems, e.g., system design and feature prioritization. Considering the significant advances in MaxSAT for Boolean logic, we develop translations from MLTL to Boolean logic to solve the MLTL MaxSAT problem. Given an MLTL formula φ of length |φ | with maximum interval length m, our first (recursive) translator runs in 𝒪(m^|φ |) time. Our second, improved (iterative) translator runs in 𝒪(|φ |^2m^2) time. Performance tests of satisfiability checks on MaxSAT instances illustrate that these Boolean translations perform significantly better than the best satisfiability checking approaches reported recently in the literature on real and random instances. Furthermore, the second translator is embarrassingly parallelizable to a factor of |φ |m . We contribute to (1) an easy-to-implement translation from MLTL to Boolean logic that runs in 𝒪(m^|φ |) time, and (2) an efficient translation that runs in 𝒪(|φ |^2m^2) time, and prove their correctness and runtime. Lastly, (3) we consider examples of using Boolean MaxSAT solvers to solve the MLTL MaxSAT problem.
A reversible computing system features backward computations along which the effects of forward ones are undone when needed. This is accomplished by reverting executed actions from the last one. Since the last performed action may not be uniquely identifiable in a concurrent system, causal reversibility is considered: an executed action can be undone provided that all of its consequences have been undone already. We investigate causal reversibility in a timed setting by defining a reversible calculus in the style of Phillips and Ulidowski in which action execution is separated from time passing, actions can be lazy or eager, and time is described via numeric delays subject to time additivity. We show that the calculus meets causal reversibility through an adaptation of the technique of Lanese, Phillips, and Ulidowski that ensures a proper treatment of action laziness/eagerness as well as time-additive delays.
Network congestion games are a simple model for reasoning about routing problems in a network. They are a very popular topic in algorithmic game theory, and a huge amount of results about existence and (in)efficiency of equilibrium strategy profiles in those games have been obtained over the last 20 years. In particular, the price of anarchy has been defined as an important notion for measuring the inefficiency of Nash equilibria. Generic bounds have been obtained for the price of anarchy over various classes of networks, but little attention has been put on the effective computation of this value for a given network. This talk presents recent results on this problem in different settings.
