Abstract Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex optimization to solve for a smooth Bézier spline that is guaranteed to satisfy a Linear Temporal Logic specification. Our approach uses a coarse abstraction to avoid the state explosion of other abstraction based methods, and successfully avoids the computational challenges of directly optimizing the non-convex temporal logic semantics. We prove our method is sound and complete and demonstrate a significant computational advantage relative to state of the art approaches. Generating such smooth paths has natural applications in path planning for autonomous robots, and we demonstrate the applicability of our method on path planning for a quadrotor.

Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

Cyber-physical systems (CPS) designed in simulators, often consisting of multiple interacting agents (e.g., in multi-agent formations), behave differently in the real-world. We would like to verify these systems during runtime when they are deployed. Thus, we propose robust predictive runtime verification (RPRV) algorithms for: (1) general stochastic CPS under signal temporal logic (STL) tasks, and (2) stochastic multi-agent systems (MAS) under spatio-temporal logic tasks. The RPRV problem presents the following challenges: (1) there may not be sufficient data on the behavior of the deployed CPS, (2) predictive models based on design phase system trajectories may encounter distribution shift during real-world deployment, and (3) the algorithms need to scale to the complexity of MAS and be applicable to spatio-temporal logic tasks. To address these challenges, we assume knowledge of an upper bound on the statistical distance (in terms of an f -divergence) between the trajectory distributions of the system at deployment and design time. We are motivated by our prior work where we proposed an accurate and an interpretable RPRV algorithm for general CPS, which we here extend to the MAS setting and spatio-temporal logic tasks. Specifically, we use a learned predictive model to estimate the system behavior at runtime and robust conformal prediction to obtain probabilistic guarantees by accounting for distribution shifts. Building on our prior work, we perform robust conformal prediction over the robust semantics of spatio-temporal reach and escape logic (STREL) to obtain centralized RPRV algorithms for MAS. We empirically validate our results in a drone swarm simulator, where we show the scalability of our RPRV algorithms to MAS and analyze the impact of different trajectory predictors on the verification result. To the best of our knowledge, these are the first statistically valid algorithms for MAS under distribution shift.

Multi-agent systems (MASs) consisting of a number of autonomous agents that communicate, coordinate, and jointly sense the environment to achieve complex missions can be found in a variety of applications such as robotics, smart cities, and internet-of-things applications. Modeling and monitoring MAS requirements to guarantee overall mission objectives, safety, and reliability is an important problem. Such requirements implicitly require reasoning about diverse sensing and communication modalities between agents, analysis of the dependencies between agent tasks, and the spatial or virtual distance between agents. To capture such rich MAS requirements, we model agent interactions via multiple directed graphs, and introduce a new logic – Spatio-Temporal Logic with Graph Operators (STL-GO). The key innovation in STL-GO are graph operators that enable us to reason about the number of agents along either the incoming or outgoing edges of the underlying interaction graph that satisfy a given property of interest; for example, the requirement that an agent should sense at least two neighboring agents whose task graphs indicate the ability to collaborate. We then propose novel distributed monitoring conditions for individual agents that use only local information to determine whether or not an STL-GO specification is satisfied. We compare the expressivity of STL-GO against existing spatio-temporal logic formalisms, and demonstrate the utility of STL-GO and our distributed monitors in a bike-sharing and a multi-drone case study.

Reinforcement learning (RL) has been successfully applied to solve the problem of finding obstacle-free paths for autonomous agents operating in stochastic and uncertain environments. However, when the underlying stochastic dynamics of the environment experiences drastic distribution shifts, the optimal policy obtained in the trained environment may be sub-optimal or may entirely fail in helping find goal-reaching paths for the agent. Approaches like domain randomization and robust RL can provide robust policies, but typically assume minor (bounded) distribution shifts. For substantial distribution shifts, retraining (either with a warm-start policy or from scratch) is an alternative approach. In this paper, we develop a novel approach called Evolutionary Robust Policy Optimization (ERPO), an adaptive re-training algorithm inspired by evolutionary game theory (EGT). ERPO learns an optimal policy for the shifted environment iteratively using a temperature parameter that controls the trade off between exploration and adherence to the old optimal policy. The policy update itself is an instantiation of the replicator dynamics used in EGT. We show that under fairly common sparsity assumptions on rewards in such environments, ERPO converges to the optimal policy in the shifted environment. We empirically demonstrate that for path finding tasks in a number of environments, ERPO outperforms several popular RL and deep RL algorithms (PPO, A3C, DQN) in many scenarios and popular environments. This includes scenarios where the RL algorithms are allowed to train from scratch in the new environment, when they are retrained on the new environment, or when they are used in conjunction with domain randomization. ERPO shows faster policy adaptation, higher average rewards, and reduced computational costs in policy adaptation.

In recent years, there has been increasing interest in using formal methods-based techniques to safely achieve temporal tasks, such as timed sequence of goals, or patrolling objectives. Such tasks are often expressed in real-time logics such as Signal Temporal Logic (STL), whereby, the logical specification is encoded into an optimization problem. Such approaches usually involve optimizing over the quantitative semantics, or robustness degree, of the logic over bounded horizons: the semantics can be encoded as mixed-integer linear constraints or into smooth approximations of the robustness degree. A major limitation of this approach is that it faces scalability challenges with respect to temporal complexity: for example, encoding long-term tasks requires storing the entire history of the system. In this paper, we present a quantitative generalization of such tasks in the form of symbolic automata objectives. Specifically, we show that symbolic automata can be expressed as matrix operators that lend themselves to automatic differentiation, allowing for the use of off-the-shelf gradient-based optimizers. We show how this helps solve the need to store arbitrarily long system trajectories, while efficiently leveraging the task structure encoded in the automaton.

Apprenticeship learning crucially depends on effectively learning rewards, and hence control policies from user demonstrations. Of particular difficulty is the setting where the desired task consists of a number of sub-goals with temporal dependencies. The quality of inferred rewards and hence policies are typically limited by the quality of demonstrations, and poor inference of these can lead to undesirable outcomes. In this paper, we show how temporal logic specifications that describe high level task objectives, are encoded in a graph to define a temporal-based metric that reasons about behaviors of demonstrators and the learner agent to improve the quality of inferred rewards and policies. Through experiments on a diverse set of robot manipulator simulations, we show how our framework overcomes the drawbacks of prior literature by drastically improving the number of demonstrations required to learn a control policy.

Humans and autonomous cyber-physical systems increasingly share physical space, for example, in industrial manufacturing, autonomous taxis, warehouses, and unmanned package delivery. This makes such autonomous CPS safety-critical because design errors can harm the people in their shared space. To enhance their own safe operation and the safety of humans around them, these CPSs typically use multiple sensor modalities to perceive the environment. Such sensor systems include RADAR, LIDAR, ultra-wideband, SONAR, odometry, GPS, and camera-based sensors to make estimations about their own state and observations of the environment. Traditionally, the observations made by different sensor streams are fused using probabilistic models such as Bayesian filters (e.g., Kalman filters). These filters make assumptions about the distribution of error between the observation and the ground truth for a given sensor and, using such assumptions, attempt to reconstruct a state estimate by computing some weighted combination of observations from multiple sensors (with possibly different error distributions). However, such assumptions can be challenging to model as environments become more complex. Furthermore, such algorithms typically do not account for sensor failures or shifts in the error distribution during deployment. This paper presents an algorithmic framework that defines a notion of spatio-temporal consistency across sensor streams. We eschew the idea of computing a fused state estimate and instead focus on producing a consistent state estimate if the multiple sensor observations are deemed consistent. If we detect an inconsistency in the state estimate, we propose a conservative over-approximation of the state estimate based on the last known consistent estimate. We demonstrate how such a framework can be deployed in an industrial manufacturing case study. We show that such a framework can provide probabilistic runtime assurance using conformal prediction techniques for statistical analyses.

Reachability analysis is a popular method to give safety guarantees for stochastic cyber-physical systems (SCPSs) that takes in a symbolic description of the system dynamics and uses set-propagation methods to compute an overapproximation of the set of reachable states over a bounded time horizon. In this article, we investigate the problem of performing reachability analysis for an SCPS that does not have a symbolic description of the dynamics, but instead is described using a digital twin model that can be simulated to generate system trajectories. An important challenge is that the simulator implicitly models a probability distribution over the set of trajectories of the SCPS; however, it is typical to have a sim2real gap, i.e., the actual distribution of the trajectories in a deployment setting may be shifted from the distribution assumed by the simulator. We thus propose a statistical reachability analysis technique that, given a user-provided threshold$1-\epsilon $, provides a set that guarantees that any trajectory during deployment lies in this set with probability not smaller than this threshold. Our method is based on three main steps: 1) learning a deterministic surrogate model from sampled trajectories; 2) conducting reachability analysis over the surrogate model; and 3) employing robust conformal inference (CI) using an additional set of sampled trajectories to quantify the surrogate model’s distribution shift with respect to the deployed SCPS. To counter conservatism in reachable sets, we propose a novel method to train surrogate models that minimizes a quantile loss term (instead of the usual mean squared loss), and a new method that provides tighter guarantees using CI using a normalized surrogate error. We demonstrate the effectiveness of our technique on various case studies.

This article introduces a model-based approach for training feedback controllers for an autonomous agent operating in a highly non-linear (albeit deterministic) environment. We desire the trained policy to ensure that the agent satisfies specific task objectives and safety constraints, both expressed in Discrete-Time Signal Temporal Logic (DT-STL). One advantage for reformulation of a task via formal frameworks, like DT-STL, is that it permits quantitative satisfaction semantics. In other words, given a trajectory and a DT-STL formula, we can compute the robustness , which can be interpreted as an approximate signed distance between the trajectory and the set of trajectories satisfying the formula. We utilize feedback control, and we assume a feed forward neural network for learning the feedback controller. We show how this learning problem is similar to training recurrent neural networks (RNNs), where the number of recurrent units is proportional to the temporal horizon of the agent’s task objectives. This poses a challenge: RNNs are susceptible to vanishing and exploding gradients, and naïve gradient descent-based strategies to solve long-horizon task objectives thus suffer from the same problems. To address this challenge, we introduce a novel gradient approximation algorithm based on the idea of dropout or gradient sampling. One of the main contributions is the notion of controller network dropout , where we approximate the NN controller in several timesteps in the task horizon by the control input obtained using the controller in a previous training step. We show that our control synthesis methodology can be quite helpful for stochastic gradient descent to converge with less numerical issues, enabling scalable back-propagation over longer time horizons and trajectories over higher-dimensional state spaces. We demonstrate the efficacy of our approach on various motion planning applications requiring complex spatio-temporal and sequential tasks ranging over thousands of timesteps.

Uncertainty in safety-critical cyber-physical systems can be modeled using a finite number of parameters or parameterized input signals. Given a system specification in Signal Temporal Logic (STL), we would like to verify that for all (infinite) values of the model parameters/input signals, the system satisfies its specification. Unfortunately, this problem is undecidable in general. Statistical model checking (SMC) offers a solution by providing guarantees on the correctness of CPS models by statistically reasoning on model simulations. We propose a new approach for statistical verification of CPS models for user-provided distribution on the model parameters. Our technique uses model simulations to learn surrogate models , and uses conformal inference to provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We compare this prediction interval with the interval we get using risk estimation procedures. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally, we demonstrate the efficacy of our technique on several CPS models.

Finding tight linear bounds for activation functions in neural networks is an essential part of several state of the art neural network robustness certification tools. An activation function is an arbitrary, nonlinear, scalar function $f: \mathbb{R}^d \rightarrow \mathbb{R}$. In the existing work on robustness certification, such bounds have been computed using human ingenuity for a handful of the most popular activation functions. While a number of heuristics have been proposed for bounding arbitrary functions, no analysis of the tightness optimality for general scalar functions has been offered yet, to the best of our knowledge. We fill this gap by formulating a concise optimality criterion for tightness of the approximation which allows us to build optimal bounds for any function convex in the region of interest $R$. For a more general class of functions Lipshitz-continuous in $R$ we propose a sampling-based approach (SOL) which, given an instance of the bounding problem, efficiently computes the tightest linear bounds within a given $\varepsilon > 0$ threshold. We leverage an adaptive sampling technique to iteratively build a set of sample points suitable for representing the target activation function. While the theoretical worst case time complexity of our approach is $O(\varepsilon^{-2d})$, it typically only takes $O(\log^{\beta} \frac{1}{\varepsilon})$ time for some $\beta \ge 1$ and is thus sufficiently fast in practice. We provide empirical evidence of SOL's practicality by incorporating it into a robustness certifier and observing that it produces similar or higher certification rates while taking as low as quarter of the time compared to the other methods.

Abstract Runtime verification (RV) refers to methods for formal reasoning about all aspects of the dynamic execution of systems, including hardware, software, and cyber-physical systems. RV includes techniques to assess and enforce correctness of a system against systemic bugs or extrinsic uncertainties. These methods are typically considered lightweight as they may not involve exhaustive verification or proofs, but they provide a higher level of rigor and versatility compared to conventional testing methods. This article introduces the extended versions of selected papers from the peer-reviewed proceedings of the 20th International Conference on Runtime Verification (RV 2020). RV 2020 was supposed to be held in Los Angeles, California, USA in July 2020, but was instead held virtually due to the global Covid-19 pandemic.

In this work, we propose the use of symbolic automata as formal specifications for reinforcement learning agents. The use of symbolic automata serves as a generalization of both bounded-time temporal logic-based specifications and deterministic finite automata, allowing us to describe input alphabets over metric spaces. Furthermore, our use of symbolic automata allows us to define non-sparse potential-based rewards which empirically shape the reward surface, leading to better convergence during RL. We also show that our potential-based rewarding strategy still allows us to obtain the policy that maximizes the satisfaction of the given specification.

Learning-from-demonstrations (LfD) is a popular paradigm to obtain effective robot control policies for complex tasks via reinforcement learning without the need to explicitly design reward functions. However, it is susceptible to imperfections in demonstrations and also raises concerns of safety and interpretability in the learned control policies. To address these issues, we propose to use Signal Temporal Logic (STL) to express high-level robotic tasks and use its quantitative semantics to evaluate and rank the quality of demonstrations. Temporal logic-based specifications allow us to create non-Markovian rewards, and are also capable of defining interesting causal dependencies between tasks such as sequential task specifications. We present our completed work that proposed LfD-STL framework that learns from even suboptimal/imperfect demonstrations and STL specifications to infer rewards for reinforcement learning tasks. We have validated our approach through various experimental setups to show how our method outperforms prior LfD methods. We then discuss future directions for tackling the problem of explainability and interpretability in such learning-based systems.

Many intelligent transportation systems are multiagent systems, i.e., both the traffic participants and the subsystems within the transportation infrastructure can be modeled as interacting agents. The use of AI-based methods to achieve coordination among the different agents systems can provide greater safety over transportation systems containing only human-operated vehicles, and also improve the system efficiency in terms of traffic throughput, sensing range, and enabling collaborative tasks. However, increased autonomy makes the transportation infrastructure vulnerable to compromised vehicular agents or infrastructure. This paper proposes a new framework by embedding the trust authority into transportation infrastructure to systematically quantify the trustworthiness of agents using an epistemic logic known as subjective logic. In this paper, we make the following novel contributions: (i) We propose a framework for using the quantified trustworthiness of agents to enable trust-aware coordination and control. (ii) We demonstrate how to synthesize trust-aware controllers using an approach based on reinforcement learning. (iii) We comprehensively analyze an autonomous intersection management (AIM) case study and develop a trust-aware version called AIM-Trust that leads to lower accident rates in scenarios consisting of a mixture of trusted and untrusted agents.

Cyber-physical system applications such as autonomous vehicles, wearable devices, and avionic systems generate a large volume of time-series data. Designers often look for tools to help classify and categorize the data. Traditional machine learning techniques for time-series data offer several solutions to solve these problems; however, the artifacts trained by these algorithms often lack interpretability. On the other hand, temporal logic, such as Signal Temporal Logic (STL) have been successfully used in the formal methods community as specifications of time-series behaviors. In this work, we propose a new technique to automatically learn temporal logic formulas that are able to classify real-valued time-series data. Previous work on learning STL formulas from data either assumes a formula-template to be given by the user, or assumes some special fragment of STL that enables exploring the formula structure in a systematic fashion. In our technique, we relax these assumptions, and provide a way to systematically explore the space of all STL formulas. As the space of all STL formulas is very large, and contains many semantically equivalent formulas, we suggest a technique to heuristically prune the space of formulas considered. Finally, we illustrate our technique on various case studies from the automotive and transportation domains.

Autonomous systems are self-governed and self-adaptive systems that must additionally comply with high assurance correctness and safety criteria. Such autonomous systems cannot be tested and verified in the traditional design process. While all systems hardware and software components can be implemented as usual, test and verification only cover the autonomous system functionality, but do not include the goal-driven autonomous behavior in all possible circumstances. This autonomous behavior is a primary design target. Thus, autonomous systems pose a number of emerging challenges and opportunities to the field of electronic design automation (EDA). Examples include specification of (evolving) requirements involving components and their interaction, defining different assurance levels for bounded operational environments, synthesis of mechanisms to guideline diagnosis and rigorously monitor systems integration after deployment.

Verification and validation are vital steps in the development process of autonomous systems such as mobile robots and self-driving vehicles, as they allow reasoning about system safety. In the domain of cyber-physical systems, techniques using formal requirements have been show to enable rigorous mathematical reasoning about system safety through techniques for automatic test generation and performance analysis. In this paper, we show that system-level and subsystem-level requirements can also enable fault localization in autonomous systems that use heterogeneous functional components. However, writing correct formal requirements is challenging and requires a significant investment of time, effort and most importantly, expertise. To address this issue, we propose a specification library for autonomous mobile systems called TLAM (Temporal Logic for Autonomous Mobility). Our contributions are twofold: We provide a library of parametric formal specifications at both the system-level and subsystem-level for typical subsystems in autonomous systems such as those for perception, planning and decision-making. The specification parameters encode the design trade-offs for such components. Second, we introduce a new fault localization technique based on these parametric specifications that identifies the likeliest subsystem that has a fault.

Shape expressions (SEs) is a novel specification language that was recently introduced to express behavioral patterns over real-valued signals observed during the execution of cyber-physical systems. An SE is a regular expression composed of arbitrary parameterized shapes, such as lines, exponential curves, and sinusoids as atomic symbols with symbolic constraints on the shape parameters. SEs enable a natural and intuitive specification of complex temporal patterns over possibly noisy data. In this article, we propose a novel method for mining a broad and interesting fragment of SEs from time-series data using a combination of techniques from linear regression, unsupervised clustering, and learning finite automata from positive examples. The learned SE for a given dataset provides an explainable and intuitive model of the observed system behavior. We demonstrate the applicability of our approach on two case studies from different application domains and experimentally evaluate the implemented specification mining procedure.

We formulate numerically-robust inductive proof rules for unbounded stability and safety properties of continuous dynamical systems. These induction rules robustify standard notions of Lyapunov functions and barrier certificates so that they can tolerate small numerical errors. In this way, numerically-driven decision procedures can establish a sound and relative-complete proof system for unbounded properties of very general nonlinear systems. We demonstrate the effectiveness of the proposed rules for rigorously verifying unbounded properties of various nonlinear systems, including a challenging powertrain control model.

Robust perception algorithms are a vital ingredient for autonomous systems such as self-driving vehicles. Checking the correctness of perception algorithms such as those based on deep convolutional neural networks (CNN) is a formidable challenge problem. In this paper, we suggest the use of Timed Quality Temporal Logic (TQTL) as a formal language to express desirable spatio-temporal properties of a perception algorithm processing a video. While perception algorithms are traditionally tested by comparing their performance to ground truth labels, we show how TQTL can be a useful tool to determine quality of perception, and offers an alternative metric that can give useful information, even in the absence of ground truth labels. We demonstrate TQTL monitoring on two popular CNNs: YOLO and SqueezeDet, and give a comparative study of the results obtained for each architecture.

Cyber-physical systems are often safety-critical in that violations of safety properties may lead to catastrophes. We propose a method to enforce the safety of systems with real-valued signals by synthesizing a runtime enforcer called the shield. Whenever the system violates a property, the shield, composed with the system, makes correction instantaneously to ensure that no erroneous output is generated by the combined system. While techniques for synthesizing Boolean shields are well understood, they do not handle real-valued signals ubiquitous in cyber-physical systems, meaning their corrections may be either unrealizable or inefficient to compute in the real domain. We solve the realizability and efficiency problems by analyzing the compatibility of predicates defined over real-valued signals, and using the analysis result to constrain a two-player safety game used to synthesize the shield. We demonstrate the effectiveness of this method on a variety of applications, including an automotive powertrain control system.

In this work we present a new method for shaping reward functions to train reinforcement learning agents using signal temporal logic (STL) formulas. The proposed approach uses the robustness metric of partial signal traces against STL specifications to generate locally shaped rewards, doing this in a manner that is agnostic of the learning algorithm used by the reinforcement learning agent.

Monitoring is an effective approach for identifying safety violations for complex cyber-physical systems. In this poster, we consider safety specifications expressed in Signal Temporal Logic (STL). STL is a logic for specifying timed properties of real-valued signals, and there has been significant work on offline and online monitoring of STL formulas on signals. Boolean monitoring techniques solve the problem of determining if a given STL formula is satisfied by a signal, while robust monitoring techniques seek to compute a quantitative degree of satisfaction of the formula. Online techniques can compute satisfaction or violation of the formula when the entire signal is not available, but existing online techniques can only provide worst-case estimates of satisfaction (or violation). In this poster, we propose algorithms to predict the satisfaction or violation of an STL formula when only partial information of a trace (i.e. its prefix) is available. The output of our algorithm is a predicted interval for the robust satisfaction value, along with a probabilistic guarantee on the correctness of the prediction. We demonstrate the utility of our approach on monitoring a safety-critical signal in the context of unmanned aerial vehicle.

There is recent interest in using deep neural networks (DNNs) for controlling autonomous cyber-physical systems (CPSs). One challenge with this approach is that many autonomous CPS applications are safety-critical, and is not clear if DNNs can proffer safe system behaviors. To address this problem, we present an approach to modify existing (deep) reinforcement learning algorithms to guide the training of those controllers so that the overall system is safe. We present a novel verification-in-the-loop training algorithm that uses the formalism of barrier certificates to synthesize DNN-controllers that are safe by design. We demonstrate a proof-of-concept evaluation of our technique on multiple CPS examples.

Deep reinforcement learning has become a popular technique to train autonomous agents to learn control policies that enable them to accomplish complex tasks in uncertain environments. A key component of an RL algorithm is the definition of a reward function that maps each state and an action that can be taken in that state to some real-valued reward. Typically, reward functions informally capture an implicit (albeit vague) specification on the desired behavior of the agent. In this paper, we propose the use of the logical formalism of Signal Temporal Logic(STL) as a formal specification for the desired behaviors of the agent. Furthermore, we propose algorithms to locally shape rewards in each state with the goal of satisfying the high-level STL specification. We demonstrate our technique on two case studies, a cart-pole balancing problem with a discrete action space, and controlling the actuation of a simulated quadrotor for point-to-point movement.The proposed framework is agnostic to any specific RL algorithm, as locally shaped rewards can be easily used in concert with any deep RL algorithm.

In this paper, we propose Stochastic Temporal Logic (StTL) as a formalism for expressing probabilistic specifications on time-varying behaviors of controlled stochastic dynamical systems. To make StTL a more effective specification formalism, we introduce the quantitative semantics for StTL to reason about the robust satisfaction of an StTL specification by a given system. Additionally, we propose using the robustness value as the objective function to be maximized by a stochastic optimization algorithm for the purpose of controller design. Finally, we formulate an algorithm for parameter inference for Parameteric-StTL specifications, which allows specifications to be mined from output traces of the underlying system. We demonstrate and validate our framework on two case studies inspired by the automotive domain.

We present a simulation-based approach for generating barrier certificate functions for safety verification of cyber-physical systems (CPS) that contain neural network-based controllers. A linear programming solver is utilized to find a candidate generator function from a set of simulation traces obtained by randomly selecting initial states for the CPS model. A level set of the generator function is then selected to act as a barrier certificate for the system, meaning it demonstrates that no unsafe system states are reachable from a given set of initial states. The barrier certificate properties are verified with an SMT solver. This approach is demonstrated on a case study in which a Dubins car model of an autonomous vehicle is controlled by a neural network to follow a given path.

Evaluation of industrial embedded control system designs is a time-consuming and imperfect process. While an ideal process would apply a formal verification technique such as model checking or theorem proving, these techniques do not scale to industrial design problems, and it is often difficult to use these techniques to verify performance aspects of control system designs, such as stability or convergence. For industrial designs, engineers rely on testing processes to identify critical or unexpected behaviors. We propose a novel framework called Underminer to improve the testing process; this is an automated technique to identify nonconverging behaviors in embedded control system designs. Underminer treats the system as a black box and lets the designer indicate the model parameters, inputs, and outputs that are of interest. It differentiates convergent from nonconvergent behaviors using Convergence Classifier Functions (CCFs). The tool can be applied in the context of testing models created late in the controller development stage, where it assumes that the given model displays mostly convergent behavior and learns a CCF in an unsupervised fashion from such convergent model behaviors. This CCF is then used to guide a thorough exploration of the model with the help of optimization-guided techniques or adaptive sampling techniques, with the goal of identifying rare nonconvergent model behaviors. Underminer can also be used early in the development stage, where models may have some significant nonconvergent behaviors. Here, the framework permits designers to indicate their mental model for convergence by labeling behaviors as convergent/nonconvergent and then constructs a CCF using a supervised learning technique. In this use case, the goal is to use the CCF to test an improved design for the model. Underminer supports a number of convergence-like notions, such as those based on Lyapunov analysis and temporal logic, and also CCFs learned directly from labeled output behaviors using machine-learning techniques such as support vector machines and neural networks. We demonstrate the efficacy of Underminer by evaluating its performance on several academic as well as industrial examples.

We present a technique to investigate abnormal behaviors of signals in both time and frequency domains using an extension of time-frequency logic that uses the continuous wavelet transform. Abnormal signal behaviors such as unexpected oscillations, called hunting behavior, can be challenging to capture in the time domain; however, these behaviors can be naturally captured in the time-frequency domain. We introduce the concept of parametric time-frequency logic and propose a parameter synthesis approach that can be used to classify hunting behavior. We perform a comparative analysis between the proposed algorithm, an approach based on support vector machines using linear classification, and a method that infers a signal temporal logic formula as a data classifier. We present experimental results based on data from a hydrogen fuel cell vehicle application and electrocardiogram data extracted from the MIT-BIH Arrhythmia Database.

A hyperproperty is a property that requires two or more execution traces to check. This is in contrast to properties expressed using temporal logics such as LTL, MTL and STL, which can be checked over individual traces. Hyperproperties are important as they are used to specify critical system performance objectives, such as those related to security, stochastic (or average) performance, and relationships between behaviors. We present the first study of hyperproperties of cyber-physical systems (CPSs). We introduce a new formalism for specifying a class of hyperproperties defined over real-valued signals, called HyperSTL. The proposed logic extends signal temporal logic (STL) by adding existential and universal trace quantifiers into STL's syntax to relate multiple execution traces. Several instances of hyperproperties of CPSs including stability, security, and safety are studied and expressed in terms of HyperSTL formulae. Furthermore, we propose a testing technique that allows us to check or falsify hyperproperties of CPS models. We present a discussion on the feasibility of falsifying or verifying various classes of hyperproperties for CPSs. We extend the quantitative semantics of STL to HyperSTL and show its utility in formulating algorithms for falsification of HyperSTL specifications. We demonstrate how we can specify and falsify HyperSTL properties for two case studies involving automotive control systems.

In recent years early life failures have caused several product recalls in semiconductor and automotive industries associated with a loss of billions of dollars. They can be traced back to various root-causes. In embedded or cyber-physical systems, the interaction with the environment and the behavior of the hardware/software interface are hard to predict, which may lead to unforeseen failures. In addition to that, defects that have escaped manufacturing test or “weak” devices that cannot stand operational stress may for example cause unexpected hardware problems in the early life of a system. The special session focuses on the first aspect. The first contribution discusses how the interaction with the environment in cyber-physical systems can be appropriately modeled and tested. The second presentation then deals with a cross-layer approach identifying problems at the hardware/software interface which cannot be compensated by the application and must therefore be targeted by specific tests.

The conformance testing problem for dynamical systems asks, given two dynamical models (e.g., as Simulink diagrams), whether their behaviors are “close” to each other. In the semi-formal approach to conformance testing, the two systems are simulated on a large set of tests, and a metric, defined on pairs of real-valued, real-timed trajectories, is used to determine a lower bound on the distance. We show how the Skorokhod metric on continuous dynamical systems can be used as the foundation for conformance testing of complex dynamical models. The Skorokhod metric allows for both state value mismatches and timing distortions, and is thus well suited for checking conformance between idealized models of dynamical systems and their implementations. We demonstrate the robustness of the metric by proving a transference theorem : trajectories close under the Skorokhod metric satisfy “close” logical properties in the timed linear time logic FLTL (Freeze LTL ) containing a rich class of temporal and spatial constraint predicates involving time and value freeze variables. We provide efficient window-based streaming algorithms to compute the Skorokhod metric for both piecewise affine and piecewise constant traces, and use these as a basis for a conformance testing tool for Simulink. We experimentally demonstrate the effectiveness of our tool in finding discrepant behaviors on a set of control system benchmarks, including an industrial challenge problem.

Many problems in the design and analysis of cyber-physical systems (CPS) reduce to the following optimization problem: given a CPS which transforms continuous-time input traces in R m to continuous-time output traces in R n and a cost function over output traces, find an input trace which minimizes the cost. Cyber-physical systems are typically so complex that solving the optimization problem analytically by examining the system dynamics is not feasible. We consider a black-box approach, where the optimization is performed by testing the input-output behaviour of the CPS. We provide a unified, tool-supported methodology for CPS testing and optimization. Our tool is the first CPS testing tool that supports Bayesian optimization. It is also the first to employ fully automated dimensionality reduction techniques. We demonstrate the potential of our tool by running experiments on multiple industrial case studies. We compare the effectiveness of Bayesian optimization to state-of-the-art testing techniques based on CMA-ES and Simulated Annealing.

Evaluation of industrial embedded control system designs is a time-consuming and imperfect process. While an ideal process would apply a formal verification technique such as model checking or theorem proving, these techniques do not scale to industrial design problems, and it is often difficult to use these techniques to verify performance aspects of control system designs, such as stability or convergence. For industrial designs, engineers rely on testing processes to identify critical or unexpected behaviors. We propose a novel framework called Underminer to improve the testing process; this is an automated technique to identify non-converging behaviors in embedded control system designs. Underminer treats the system as a black box, and lets the designer indicate the model parameters, inputs and outputs that are of interest. It supports a multiplicity of convergence-like notions, such as those based on Lyapunov analysis and those based on temporal logic formulae. Underminer can be applied in the context of testing models created in the controller-design phase, and can also be applied in a scenario such as hardware-in-the-loop testing. We demonstrate the efficacy of Underminer by evaluating its performance on several examples.

We study the problem of falsifying reachability properties of real-time control software acting in a closed-loop with a given model of the plant dynamics. Our approach employs numerical techniques to simulate a plant model, which may be highly nonlinear and hybrid, in combination with symbolic simulation of the controller software. The state-space and input-space of the plant are systematically searched using a plant abstraction that is implicitly defined by ``quantization'' of the plant state, but never explicitly constructed. Simultaneously, the controller behaviors are explored using a symbolic execution of the control software. On-the-fly exploration of the overall closed-loop abstraction results in abstract counterexamples, which are used to refine the plant abstraction iteratively until a concrete violation is found. Empirical evaluation of our approach shows its promise in treating controller software that has precise, formal semantics, using an exact method such as symbolic execution, while using numerical simulations to produce abstractions of the underlying plant model that is often an approximation of the actual plant. We also discuss a preliminary comparison of our approach with techniques that are primarily simulation-based.

The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems; however, state-of-the-art theorem provers require manual intervention to handle complex systems. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide directly. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about performance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage forward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing automatic verification approaches using several examples, including one involving an automotive powertrain control system.

We present a search technique to falsify safety properties of hybrid systems that model a software system controlling a physical plant. Our approach takes as input (a) the controller code and (b) a plant model given as a black-box system that can be simulated for given inputs over finite time horizons. Our approach combines the symbolic execution of the controller software with an abstraction of the plant, which is discovered on-the-fly using simulations. This process is used to find abstract counterexamples to the safety properties of interest. The plant abstraction is then refined iteratively using the abstract counterexamples until a concrete violation is discovered. Empirical evaluation of our approach shows its promise in treating controller software, whose semantics are well-understood using formal techniques while using numerical simulations to produce abstractions of the underlying plant model, which is often an approximation of the actual plant.

Formal verification of a control system can be performed by checking if a model of its dynamical behavior conforms to temporal requirements. Unfortunately, adoption of formal verification in an industrial setting is a formidable challenge as design requirements are often vague, nonmodular, evolving, or sometimes simply unknown. We propose a framework to mine requirements from a closed-loop model of an industrial-scale control system, such as one specified in Simulink. The input to our algorithm is a requirement template expressed in parametric signal temporal logic: a logical formula in which concrete signal or time values are replaced with parameters. Given a set of simulation traces of the model, our method infers values for the template parameters to obtain the strongest candidate requirement satisfied by the traces. It then tries to falsify the candidate requirement using a falsification tool. If a counterexample is found, it is added to the existing set of traces and these steps are repeated; otherwise, it terminates with the synthesized requirement. Requirement mining has several usage scenarios: mined requirements can be used to formally validate future modifications of the model, they can be used to gain better understanding of legacy models or code, and can also help enhancing the process of bug finding through simulations. We demonstrate the scalability and utility of our technique on three complex case studies in the domain of automotive powertrain systems: a simple automatic transmission controller, an air-fuel controller with a mean-value model of the engine dynamics, and an industrial-size prototype airpath controller for a diesel engine. We include results on a bug found in the prototype controller by our method.

In this paper, we present an approach for finding violations of safety properties of hybrid systems. Existing approaches search for complete system trajectories that begin from an initial state and reach some unsafe state. We present an approach that searches over segmented trajectories, consisting of a sequence of segments starting from any system state. Adjacent segments may have gaps, which our approach then seeks to narrow iteratively. We show that segmented trajectories are actually paths in the abstract state graph obtained by tiling the state space with cells. Instead of creating the prohibitively large abstract state graph explicitly, our approach implicitly performs a randomized search on it using a scatter-and-simulate technique. This involves repeated simulations, graph search to find likeliest abstract counterexamples, and iterative refinement of the abstract state graph. Finally, we demonstrate our technique on a number of case studies ranging from academic examples to models of industrial-scale control systems.

Industrial control systems are often hybrid systems that are required to satisfy strict performance requirements. Verifying designs against requirements is a difficult task, and there is a lack of suitable open benchmark models to assess, evaluate, and compare tools and techniques. Benchmark models can be valuable for the hybrid systems research community, as they can communicate the nature and complexity of the problems facing industrial practitioners. We present a collection of benchmark problems from the automotive powertrain control domain that are focused on verification for hybrid systems; the problems are intended to challenge the research community while maintaining a manageable scale. We present three models of a fuel control system, each with a unique level of complexity, along with representative requirements in signal temporal logic (STL). We provide results obtained by applying a state of the art analysis tool to these models, and finally, we discuss challenge problems for the research community.

Lyapunov functions are used to prove stability and to obtain performance bounds on system behaviors for nonlinear and hybrid dynamical systems, but discovering Lyapunov functions is a difficult task in general. We present a technique for discovering Lyapunov functions and barrier certificates for nonlinear and hybrid dynamical systems using a search-based approach. Our approach uses concrete executions, such as those obtained through simulation, to formulate a series of linear programming (LP) optimization problems; the solution to each LP creates a candidate Lyapunov function. Intermediate candidates are iteratively improved using a global optimizer guided by the Lie derivative of the candidate Lyapunov function. The analysis is refined using counterexamples from a Satisfiability Modulo Theories (SMT) solver. When no counterexamples are found, the soundness of the analysis is verified using an arithmetic solver. The technique can be applied to a broad class of nonlinear dynamical systems, including hybrid systems and systems with polynomial and even transcendental dynamics. We present several examples illustrating the efficacy of the technique, including two automotive powertrain control examples.

A significant challenge to the formal validation of software-based industrial control systems is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. We propose a framework for mining requirements from the closed-loop model of an industrial-scale control system, such as one specified in the Simulink modeling language. The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic --- a formalism to express temporal formulas in which concrete signal or time values are replaced by parameters. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool. The algorithm terminates when no counterexample is found. Mining has many usage scenarios: mined requirements can be used to validate future modifications of the model, they can be used to enhance understanding of legacy models, and can also guide the process of bug-finding through simulations. We present two case studies for requirement mining: a simple automobile transmission controller and an industrial airpath control model for an engine.

We propose a deterministic model for associating costs with strings that is parameterized by operations of interest (such as addition, scaling, and minimum), a notion of regularity that provides a yardstick to measure expressiveness, and study decision problems and theoretical properties of resulting classes of cost functions. Our definition of regularity relies on the theory of string-to-tree transducers, and allows associating costs with events that are conditioned on regular properties of future events. Our model of cost register automata allows computation of regular functions using multiple “write-only” registers whose values can be combined using the allowed set of operations. We show that the classical shortest-path algorithms as well as the algorithms designed for computing discounted costs can be adapted for solving the min-cost problems for the more general classes of functions specified in our model. Cost register automata with the operations of minimum and increment give a deterministic model that is equivalent to weighted automata, an extensively studied nondeterministic model, and this connection results in new insights and new open problems.

With the maturing of technology for model checking and constraint solving, there is an emerging opportunity to develop programming tools that can transform the way systems are specified. In this paper, we propose a new way to program distributed protocols using concolic snippets. Concolic snippets are sample execution fragments that contain both concrete and symbolic values. The proposed approach allows the programmer to describe the desired system partially using the traditional model of communicating extended finite-state-machines (EFSM), along with high-level invariants and concrete execution fragments. Our synthesis engine completes an EFSM skeleton by inferring guards and updates from the given fragments which is then automatically analyzed using a model checker with respect to the desired invariants. The counterexamples produced by the model checker can then be used by the programmer to add new concrete execution fragments that describe the correct behavior in the specific scenario corresponding to the counterexample.

Programs that manipulate heap-allocated data structures present a formidable challenge for algorithmic verification. Recursive procedures (methods) in such software libraries are used for a large number of tasks ranging from simple traversals to complex structural transformations. Verification of such methods is undecidable in general. Hence, we present a programming language fragment with a syntax similar to that of C for which correctness can be algorithmically checked. For methods written in our fragment, and specifications in the form of tree automata, verification is efficient in most cases, as illustrated by our prototype tool. Our framework can be used to verify methods such as insertion and deletion of nodes in k-ary trees, binary search trees, linked lists, linked list reversal, and rotations in balanced trees, with respect to specifications such as acyclicity, sortedness, list-ness, tree-ness, and absence of null pointer dereferences.

Methods in object-oriented concurrent libraries hide internal synchronization details. However, information hiding may result in clients causing thread safety violations by invoking methods in an unsafe manner. Given such a library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments, such that the derived contracts guarantee deadlock free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of the client code.

Automatic techniques for software verification focus on obtaining witnesses of program failure. Such counterexamples often fail to localize the precise cause of an error and usually do not suggest a repair strategy. We present an efficient algorithm to automatically generate a repair for an incorrect sequential Boolean program where program correctness is specified using a pre-condition and a post-condition. Our approach draws on standard techniques from predicate calculus to obtain annotations for the program statements. These annotations are then used to generate a synthesis query for each program statement, which if successful, yields a repair. Furthermore, we show that if a repair exists for a given program under specified conditions, our technique is always able to find it.