No Arabic abstract
The development of safety-critical systems requires the control of hazards that can potentially cause harm. To this end, safety engineers rely during the development phase on architectural solutions, called safety patterns, such as safety monitors, voters, and watchdogs. The goal of these patterns is to control (identified) faults that can trigger hazards. Safety patterns can control such faults by e.g., increasing the redundancy of the system. Currently, the reasoning of which pattern to use at which part of the target system to control which hazard is documented mostly in textual form or by means of models, such as GSN-models, with limited support for automation. This paper proposes the use of logic programming engines for the automated reasoning about system safety. We propose a domain-specific language for embedded system safety and specify as disjunctive logic programs reasoning principles used by safety engineers to deploy safety patterns, e.g., when to use safety monitors, or watchdogs. Our machinery enables two types of automated safety reasoning: (1) identification of which hazards can be controlled and which ones cannot be controlled by the existing safety patterns; and (2) automated recommendation of which patterns could be used at which place of the system to control potential hazards. Finally, we apply our machinery to two examples taken from the automotive domain: an adaptive cruise control system and a battery management system.
This paper considers the problem of safety controller synthesis for systems equipped with sensor modalities that can provide preview information. We consider switched systems where switching mode is an external signal for which preview information is available. In particular, it is assumed that the sensors can notify the controller about an upcoming mode switch before the switch occurs. We propose preview automaton, a mathematical construct that captures both the preview information and the possible constraints on switching signals. Then, we study safety control synthesis problem with preview information. An algorithm that computes the maximal invariant set in a given mode-dependent safe set is developed. These ideas are demonstrated on two case studies from autonomous driving domain.
A method is presented to learn neural network (NN) controllers with stability and safety guarantees through imitation learning (IL). Convex stability and safety conditions are derived for linear time-invariant plant dynamics with NN controllers by merging Lyapunov theory with local quadratic constraints to bound the nonlinear activation functions in the NN. These conditions are incorporated in the IL process, which minimizes the IL loss, and maximizes the volume of the region of attraction associated with the NN controller simultaneously. An alternating direction method of multipliers based algorithm is proposed to solve the IL problem. The method is illustrated on an inverted pendulum system, aircraft longitudinal dynamics, and vehicle lateral dynamics.
Control schemes for autonomous systems are often designed in a way that anticipates the worst case in any situation. At runtime, however, there could exist opportunities to leverage the characteristics of specific environment and operation context for more efficient control. In this work, we develop an online intermittent-control framework that combines formal verification with model-based optimization and deep reinforcement learning to opportunistically skip certain control computation and actuation to save actuation energy and computational resources without compromising system safety. Experiments on an adaptive cruise control system demonstrate that our approach can achieve significant energy and computation savings.
The security of billions of devices worldwide depends on the security and robustness of the mainline Linux kernel. However, the increasing number of kernel-specific vulnerabilities, especially memory safety vulnerabilities, shows that the kernel is a popular and practically exploitable target. Two major causes of memory safety vulnerabilities are reference counter overflows (temporal memory errors) and lack of pointer bounds checking (spatial memory errors). To succeed in practice, security mechanisms for critical systems like the Linux kernel must also consider performance and deployability as critical design objectives. We present and systematically analyze two such mechanisms for improving memory safety in the Linux kernel: (a) an overflow-resistant reference counter data structure designed to accommodate typical reference counter usage in kernel source code, and (b) runtime pointer bounds checking using Intel MPX in the kernel.
With safety being one of the primary motivations for developing automated vehicles (AVs), extensive field and simulation tests are being carried out to ensure AVs can operate safely on roadways. Since 2014, the California DMV has been collecting AV collision and disengagement reports, which are valuable data sources for studying AV crash patterns. In this study, crash sequence data extracted from California AV collision reports were used to investigate patterns and how they may be used to develop AV test scenarios. Employing sequence analysis, this study evaluated 168 AV crashes (with AV in automatic driving mode before disengagement or collision) from 2015 to 2019. Analysis of subsequences showed that the most representative pattern in AV crashes was (collision following AV stop) type. Analysis of event transition showed that disengagement, as an event in 24 percent of all studied AV crash sequences, had a transition probability of 68 percent to an immediate collision. Cluster analysis characterized AV crash sequences into seven groups with distinctive crash dynamic features. Cross-tabulation analysis showed that sequence groups were significantly associated with variables measuring crash outcomes and describing environmental conditions. Crash sequences are useful for developing AV test scenarios. Based on the findings, a scenario-based AV safety testing framework was proposed with sequence of events embedded as a core component.