Abstract Deep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact abstraction whose transition probabilities are computed from the confusion matrices measuring the performance of the DNN on a representative image data set. As the probabilities are estimated based on empirical data, and thus are subject to error, we also compute confidence intervals in addition to point estimates for these probabilities and thereby strengthen the soundness of the analysis. We also show how to leverage local, DNN-specific analyses as run-time guards to filter out mis-behaving inputs and increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception.

Abstract Applying standard software engineering practices to neural networks is challenging due to the lack of high-level abstractions describing a neural network’s behavior. To address this challenge, we propose to extract high-level task-specific features from the neural network internal representation, based on monitoring the neural network activations. The extracted feature representations can serve as a link to high-level requirements and can be leveraged to enable fundamental software engineering activities, such as automated testing, debugging, requirements analysis, and formal verification, leading to better engineering of neural networks. Using two case studies, we present initial empirical evidence demonstrating the feasibility of our ideas.

Deep learning (DL) models are becoming effective in solving computer-vision tasks such as semantic segmentation, object tracking, and pose estimation on real-world captured images. Reliability analysis of autonomous systems that use these DL models as part of their perception systems have to account for the performance of these models. Autonomous systems with traditional sensors have tried-and-tested reliability assessment processes with modular design, unit tests, system integration, compositional verification, certification, etc. In contrast, DL perception modules relies on data-driven or learned models. These models do not capture uncertainty and often lack robustness. Also, these models are often updated throughout the lifecycle of the product when new data sets become available. However, the integration of an updated DL-based perception requires a reboot and start afresh of the reliability assessment and operation processes for autonomous systems. In this paper, we discuss three challenges related to specifying, verifying, and operating systems that incorporate DL-based perception. We illustrate these challenges through two concrete and open source examples.

Due to the probabilistic and uncertain nature of learning-enabled autonomous systems, new assurance technologies appropriate for such systems are becoming critical for their acceptance. Runtime monitors are among the key assurance technologies to address these challenges. In the DARPA Assured Autonomy program, our Boeing team is performing autonomous platform integration and assurance technology evaluation. In this paper, we present our preliminary evaluation results for runtime monitor technologies, which were developed by our three partner teams during Phase I for learning-enabled autonomous systems. The evaluation was completed using a flight simulator and real platforms. In the evaluation, the demonstrated assurance technologies showed significant promise in addressing the assurance shortfall currently facing learning enabled cyber physical systems, and the evaluation approach defined here provides a solid starting point for evaluations of the maturing assurance technologies in the future phases of the DARPA Assured Autonomy project.

No abstract available.

The papers from this special section addresses the topic of sustainable cyber-physical systems (CPSs). The research on CPSs addresses the close interactions between the cyber computational components and the physical components spanning from mechanical components, energy systems, human activities, to surrounding environment. CPS is expected to play a major role in the development of next-generation smart energy systems and data centers. Innovative computational methodologies such as green and energy efficient cyber-physical system design have become critical to enable the sustainable development of such systems. These technologies can be used to tackle various sustainability challenges, such as the reduction of energy induced from the large scale data center computing infrastructures, the improvement of computational efficiency in smart energy systems and connected vehicle systems, and the exploration of the renewable energy resources to mitigate classical energy usages.

Due to their safety-critical nature, cyber-physical systems (CPS) must tolerate faults and security attacks to remain fail-operational. However, conventional techniques for improving safety, such as testing and validation, do not meet this requirement, as shown by many of the real-world system failures in recent years, often with major economic and public-safety implications. We aim to improve the safety of critical CPS through synthesis of runtime enforcers, named safety guards, which are reactive components attached to the original systems to protect them against catastrophic failures. That is, even if the system occasionally malfunctions due to unknown defects, transient errors, or malicious attacks, the guard always reacts instantaneously to ensure that the combined system satisfies a predefined set of safety properties, and the deviation from the original system is kept at minimum. We illustrate the main ideas of this approach with examples, discuss the advantages compared to existing approaches, and point out some research challenges.

Safety is traditionally the most relevant property for automotive systems, and it is further enhanced by Advanced Driver Assistance Systems (ADAS) in modern automotive systems. To support ADAS and other advanced autonomous functions, automotive electronic systems become more distributed and connected than ever, with in-vehicle architecture or Vehicle-to-X (V2X) communication. These connections create a variety of interfaces which become breeding grounds for security attacks. Accordingly, security becomes a rising issue for automotive systems. In this paper, we address safety and security together, especially their interactions, in Ethernet-based automotive networks which are believed to be the next-generation automotive networks since they are able to provide high bandwidths, certain timing guarantees, and well-developed technologies. We discuss the interactions between safety and security in three problems: secret key management, frame replication and elimination, and Virtual Local Area Network (VLAN) segmentation. We demonstrate that safety and security can work together, but sometimes there is a trade-off between them. This indicates that safety cannot stand alone without considering security, and network security is a necessary component of system security. Towards safer and securer automotive systems, safety and security should be considered together during design stages of automotive systems.

Today's automotive industry is making a bold move to equip vehicles with intelligent driver assistance features. A modern automobile is now equipped with a powerful computing platform to run multiple machine learning algorithms for environment perception (e.g., pedestrian detection) and motion control (e.g., vehicle stabilization). These machine learning systems must be highly robust with extremely small failure rate in order to ensure safe and reliable driving. In this paper, we propose a novel Subset Sampling (SUS) algorithm to efficiently validate a machine learning system. In particular, a Markov Chain Monte Carlo algorithm based on graph mapping is developed to accurately estimate the rare failure rate with a minimal amount of test data, thereby minimizing the validation cost. Our numerical experiments show that SUS achieves 15.2× runtime speed-up over the conventional brute-force Monte Carlo method.

Next-generation autonomous and semi-autonomous vehicles will not only precept the environment with their own sensors, but also communicate with other vehicles and surrounding infrastructures for vehicle safety and transportation efficiency. The design, analysis and validation of various vehicle-to-vehicle (V2V) and vehicle-to-infrastructure (V2I) applications involve multiple layers, from V2V/V2I communication networks down to software and hardware of individual vehicles, and concern with stringent requirements on multiple metrics such as timing, security, reliability and fault tolerance. To cope with these challenges, we have been developing CONVINCE, a cross-layer modeling, exploration and validation framework for connected vehicles. The framework includes mathematical models, synthesis and validation algorithms, and a heterogeneous simulator for inter-vehicle communications and intra-vehicle software and hardware in a holistic environment. It explores various design options with respect to constraints and objectives on system safety, security, reliability, cost, etc. A V2V application is used in the case study to demonstrate the effectiveness of the proposed framework.

Model-Based Engineering (MBE) is a promising approach to cope with the challenges of designing the next-generation automotive systems. The increasing complexity of automotive electronics, the platform, distributed real-time embedded software, and the need for continuous evolution from one generation to the next has necessitated highly productive design approaches. However, heterogeneity, interoperability, and the lack of formal semantic underpinning in modeling, integration, validation and optimization make design automation a big challenge, which becomes a hindrance to the wider application of MBE in the industry. This paper briefly presents the interoperability challenges in the context of MBE and summarizes our current contribution to address these challenges with regard to automotive control software systems. A novel model-based formal integration framework is being developed to enable architecture modeling, timing specification, formal semantics, design by contract and optimization in the system-level design. The main advantages of the proposed approach include its pervasive use of formal methods, architecture analysis and design language (AADL) and associated tools, a novel timing annex for AADL with an expressive timing relationship language, a formal contract language to express component-level requirements and validation of component integration, and the resulting high assurance system delivery.

High-level architecture modeling languages, such as Architecture Analysis & Design Language (AADL), are gradually adopted in the design of embedded systems so that design choice verification, architecture exploration, and system property checking are carried out as early as possible. This paper presents our recent contributions to cope with clock-based timing analysis and validation of software architectures specified in AADL. In order to avoid semantics ambiguities of AADL, we mainly consider the AADL features related to real-time and logical time properties. We endue them with a semantics in the polychronous model of computation; this semantics is quickly reviewed. The semantics enables timing analysis, formal verification and simulation. In addition, thread-level scheduling, based on affine clock relations is also briefly presented here. A tutorial avionic case study, provided by C-S, has been adopted to illustrate our overall contribution.

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) defines a mathematically expressive model of time, the Clock Constraint Specification Language (CCSL), to specify timed annotations on UML diagrams and thus provides them with formally defined timed interpretations. Thanks to its expressive capability, the CCSL allows for the specification of static and dynamic properties, of deterministic and non-deterministic behaviors, or of systems with multiple clock domains. Code generation from such multi-clocked specifications (for the purpose of synthesizing a simulator, for instance) is known to be a difficult issue. We address it by using the approach of controller synthesis. In our framework, a timed CCSL specification is regarded as a property whose satisfaction should be enforced for any UML diagram carrying it as annotation. To do so, CCSL statements are first translated into dynamical polynomial systems. Such systems can be manipulated using the model-checker Sigali to synthesize an executable property (a controller) which enforces the satisfaction of the specified timing constraints on the UML diagram with which it is executed.

This paper presents an approach for the modeling and formalvalidation of high-performance systems. The approach relies on the repetitive model of computation used to express the parallelism of such systems within the Gaspard framework, which is dedicated to the codesign of high-performance system-on-chip. The system descriptions obtained with this model are then projected on the synchronous model of computation. The result of this projectionconsists of an equational model that allows one to formally analyze clock synchronizability issues so as to guarantee the reliable deployment of systems on platforms.

Tolerating the value failures of sensors is an important problem in automated control processes and plants. In this paper, we address this problem in a theoretical framework in order to demonstrate the feasibility of an automatic method based on discrete controller synthesis. We consider a fault-intolerant program whose job is to control an automated process, here a liquid tank equipped with level sensors that can be subject to value faults. This fault-intolerant program is modeled as a finite labeled transition system. We then specify formally a fault hypothesis, i.e., how many sensors can fail simultaneously. We use discrete controller synthesis to obtain automatically a program, having the same behavior as the initial fault-intolerant one, and satisfying the fault tolerance requirements under the fault hypothesis. We advocate that, thanks to the use of discrete controller synthesis, our method offers flexibility, reliability, separation of concern, and it is automatic.