We study the problem of safety verification of direct perception neural networks, where camera images are used as inputs to produce high-level features for autonomous vehicles to make control decisions. Formal verification of direct perception neural networks is extremely challenging, as it is difficult to formulate the specification that requires characterizing input as constraints, while the number of neurons in such a network can reach millions. We approach the specification problem by learning an input property characterizer which carefully extends a direct perception neural network at close-to-output layers, and address the scalability problem by a novel assume-guarantee based verification approach. The presented workflow is used to understand a direct perception neural network (developed by Audi) which computes the next waypoint and orientation for autonomous vehicles to follow.

Can engineering neural networks be approached in a disciplined way similar to how engineers build software for civil aircraft? We present nn-dependability-kit, an open-source toolbox to support safety engineering of neural networks for autonomous driving systems. The rationale behind nn-dependability-kit is to consider a structured approach (via Goal Structuring Notation) to argue the quality of neural networks. In particular, the tool realizes recent scientific results including (a) novel dependability metrics for indicating sufficient elimination of uncertainties in the product life cycle, (b) formal reasoning engine for ensuring that the generalization does not lead to undesired behaviors, and (c) runtime monitoring for reasoning whether a decision of a neural network in operation is supported by prior similarities in the training data. A proprietary version of nn-dependability-kit has been used to improve the quality of a level-3 autonomous driving component developed by Audi for highway maneuvers.

Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all- important NN dependability attributes. We address this challenge by proposing a number of NN-specific and efficiently computable metrics for measuring NN dependability attributes including robustness, interpretability, completeness, and correctness.

Safety-critical systems need to maintain their functionality in the presence of multiple errors caused by component failures or disastrous environment events. We propose a game-theoretic foundation for synthesizing control strategies that maximize the resilience of a software system in defense against a realistic error model. The new control objective of such a game is called $k$ -resilience. In order to be $k$ -resilient, a system needs to rapidly recover from infinitely many waves of a small number of up to $k$ close errors provided that the blocks of up to $k$ errors are separated by short time intervals, which can be used by the system to recover. We first argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We then show how the analysis of $k$ -resilience problems can be formulated as a model-checking problem of a mild extension to the alternating-time $\mu$ -calculus (AMC). The witness for $k$ resilience, which can be provided by the model checker, can be used for providing control strategies that are optimal with respect to resilience. We show that the computational complexity of constructing such optimal control strategies is low and demonstrate the feasibility of our approach through an implementation and experimental results.

We propose an extension to ATL ( alternating-time temporal logic ), called BSIL ( basic strategy-interaction logic ), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL + but incomparable with ATL * , GL ( game logic ), and AMC ( alternating μ-calculus ) in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We establish that the BSIL model-checking problem is PSPACE-complete. However, BSIL model checking can be performed in time quadratic in the model for fixed formulas. The BSIL (and hence ATL + ) satisfiability is 2EXPTIME-complete. Finally, we report our experiment with a model checker for BSIL.