Neural networks are vulnerable to adversarial perturbations: slight changes to inputs that can result in unexpected outputs. In neural network control systems, these inputs are often noisy sensor readings. In such settings, natural sensor noise – or an adversary who can manipulate them – may cause the system to fail. In this paper, we introduce the first technique to provably compute the minimum magnitude of sensor noise that can cause a neural network control system to violate a safety property from a given initial state. Our algorithm constructs a tree of possible successors with increasing noise until a specification is violated. We build on open-loop neural network verification methods to determine the least amount of noise that could change actions at each step of a closed-loop execution. We prove that this method identifies the unsafe trajectory with the least noise that leads to a safety violation. We evaluate our method on four systems: the Cart Pole and LunarLander environments from OpenAI gym, an aircraft collision avoidance system based on a neural network compression of ACAS Xu, and the SafeRL Aircraft Rejoin scenario. Our analysis produces unsafe trajectories where deviations under $1{\rm{\% }}$ of the sensor noise range make the systems behave erroneously.

To address the question of how to deliver time-sensitive software for cyber-physical systems (CPS) requires a range of modelling and analysis techniques to be developed and integrated. A number of these required techniques are unique to time-sensitive software where timeliness is a correctness property rather than a performance attribute. This paper focuses on how to obtain worst-case estimates of the software’s execution time; in particular, it considers how workload models are derived from assumptions about the system’s run-time behaviour. The specific contribution of this paper is the exploration of the notion that a system can be subject to more than one workload model. Examples illustrate how such multi-models can lead to improved schedulability and hence more efficient CPS. An important property of the approach is that the derived analysis exhibits model-bounded behaviour. This ensures that the maximum load on the system is never higher than that implied by the individual models.

The robots of tomorrow should be endowed with the ability to adapt to drastic and unpredicted changes in their environment and interactions with humans. Such adaptations, however, cannot be boundless: the robot must stay trustworthy. So, the adaptations should not be just a recovery into a degraded functionality. Instead, they must be true adaptations: the robot must change its behaviour while maintaining or even increasing its expected performance and staying at least as safe and robust as before. The RoboSAPIENS project will focus on autonomous robotic software adaptations and will lay the foundations for ensuring that they are carried out in an intrinsically trustworthy, safe and efficient manner, thereby reconciling open-ended self-adaptation with safety by design. RoboSAPIENS will transform these foundations into ‘first time right’-design tools and platforms and will validate and demonstrate them.

We study the problem of fitting a piecewise affine (PWA) function to input–output data. Our algorithm divides the input domain into finitely many regions whose shapes are specified by a user-provided template and such that the input–output data in each region are fit by an affine function within a user-provided error tolerance. We first prove that this problem is NP-hard. Then, we present a top-down algorithmic approach for solving the problem. The algorithm considers subsets of the data points in a systematic manner, trying to fit an affine function for each subset using linear regression. If regression fails on a subset, the algorithm extracts a minimal set of points from the subset (an unsatisfiable core) that is responsible for the failure. The identified core is then used to split the current subset into smaller ones. By combining this top-down scheme with a set-covering algorithm, we derive an overall approach that provides optimal PWA models for a given error tolerance, where optimality refers to minimizing the number of pieces of the PWA model. We demonstrate our approach on three numerical examples that include PWA approximations of a widely used nonlinear insulin–glucose regulation model and a double inverted pendulum with soft contacts.

Controller synthesis offers a correct-by-construction methodology to ensure the correctness and reliability of safety-critical cyber-physical systems (CPS). Controllers are classified based on the types of controls they employ, which include reset controllers, feedback controllers and switching logic controllers. Reset controllers steer the behavior of a CPS to achieve system objectives by restricting its initial set and redefining its reset map associated with discrete jumps. Although the synthesis of feedback controllers and switching logic controllers has received considerable attention, research on reset controller synthesis is still in its early stages, despite its theoretical and practical significance. This paper outlines our recent efforts to address this gap. Our approach reduces the problem to computing differential invariants and reach-avoid sets. For polynomial CPS, the resulting problems can be solved by further reduction to convex optimizations. Moreover, considering the inevitable presence of time delays in CPS design, we further consider synthesizing reset controllers for CPS that incorporate delays.