Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving vehicles. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies requires the development of methodologies to guarantee and monitor safe operation. Despite the paramount importance of perception systems, currently there is no formal approach for system-level monitoring. In this work, we propose a mathematical model for runtime monitoring and fault detection and identification in perception systems. Towards this goal, we draw connections with the literature on diagnosability in multiprocessor systems, and generalize it to account for modules with heterogeneous outputs that interact over time. The resulting temporal diagnostic graphs (i) provide a framework to reason over the consistency of perception outputs -- across modules and over time -- thus enabling fault detection, (ii) allow us to establish formal guarantees on the maximum number of faults that can be uniquely identified in a given perception systems, and (iii) enable the design of efficient algorithms for fault identification. We demonstrate our monitoring system, dubbed PerSyS, in realistic simulations using the LGSVL self-driving simulator and the Apollo Auto autonomy software stack, and show that PerSyS is able to detect failures in challenging scenarios (including scenarios that have caused self-driving car accidents in recent years), and is able to correctly identify faults while entailing a minimal computation overhead (< 5ms on a single-core CPU).

Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving cars. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies relies on the development of methodologies to guarantee and monitor safe operation as well as detect and mitigate failures. Despite the paramount importance of perception systems, currently there is no formal approach for system-level monitoring. In this work, we propose a mathematical model for runtime monitoring and fault detection of perception systems. Towards this goal, we draw connections with the literature on self-diagnosability for multiprocessor systems, and generalize it to (i) account for modules with heterogeneous outputs, and (ii) add a temporal dimension to the problem, which is crucial to model realistic perception systems where modules interact over time. This contribution results in a graph-theoretic approach that, given a perception system, is able to detect faults at runtime and allows computing an upper-bound on the number of faulty modules that can be detected. Our second contribution is to show that the proposed monitoring approach can be elegantly described with the language of topos theory, which allows formulating diagnosability over arbitrary time intervals.

This article contains an overview of recent and ongoing projects at Boeing's Huntsville Advanced Computing Group (ACG). In addition, it contains an overview of some of the work being conducted by Boeing's Advanced Civil Space Systems Group. One aspect of ACG's charter is to support the efforts of other groups at Boeing. Thus, AI is not considered a stand-alone field but, instead, is considered an area that can be used to find both long-and shortterm solutions for Boeing and its customers. All the projects listed here represent a team effort on the part of both ACG researchers and members of other Boeing organizations. Its goal was to act as a satellite laboratory for the Advanced Technology Center (now Computer Science) at the Seattle facility. It represented an effort to facilitate AI technology transfer from the Seattle laboratory to the Huntsville facilities. This satellite center was to support local Boeing organizations and their customers (primarily the National Aeronautics and ...

In this paper, we propose an approach to ensure the diagnosability of a partially controllable system. Given a model of correct and faulty behaviors of a partially observable discrete event system, equipped with a set of elementary actions that do not intertwine with autonomous events, we search a diagnosability plan, i.e., a sequence of applicable actions that leads the system from an initial belief state (a set of potentially current states) to a diagnosable belief state, in which the system is then left to run freely. This helps in reducing the diagnosis interaction with running systems and can be applied, e.g., on the output of a repair plan, like in power networks. The two successive stages of this approach keep diagnosability planning, including diagnosability tests, in PSpace in comparison to the Exptime test for the more complex active diagnosability used usually in such cases. For this, we propose to construct incrementally the twin plant structure of the given system and to exploit its parts already constructed while testing the candidate plans and constructing its next parts. This helps in pruning the twin plant constructions and many non-diagnosability plan tests. We have created a special benchmark and tested three proposed methods, according to the recycling level of twin plants construction, with one cost function used for plan optimality and an optional heuristics.

Timed Failure Propagation Graphs (TFPGs) are a formalism used in industry to describe failure propagation in a dynamic partially observable system. TFPGs are commonly used to perform model-based diagnosis. As in any model-based diagnosis approach, however, the quality of the diagnosis strongly depends on the quality of the model. Approaches to certify the quality of the TFPG are limited and mainly rely on testing. In this work we address this problem by leveraging efficient Satisfiability Modulo Theories (SMT) engines to perform exhaustive reasoning on TFPGs. We apply model-checking techniques to certify that a given TFPG satisfies (or not) a property of interest. Moreover, we discuss the problem of refinement and diagnosability testing and empirically show that our technique can be used to efficiently solve them.

Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. Diagnosability directly depends on the availability of observations, and can be guaranteed by different sets of sensors, possibly associated with different costs. In this paper, we tackle the problem of synthesizing observability requirements, i.e. automatically discovering a set of observations that is sufficient to guarantee diagnosability. We propose a novel approach with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and enables ranking configurations of observables in terms of cost, minimality, and diagnosability delay. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an efficient implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of benchmarks taken from the aerospace domain.

We propose a theory of abstraction of discrete-event systems (DES) formulated at the semantic level, i.e., as a function that maps event traces at the original (ground) level to traces at the abstract level. We study how diagnosis of DES can be performed using an abstract model, and under which conditions this process leads to a correct solution (i.e., a set of alternative diagnoses that include the real status of the system). Finally, we study how the use of an abstract model can affect the precision of diagnosis, i.e., the presence of spurious system states in the solution. To this end, we introduce the notion of diagnosability with abstract models, which ensures the precision of abstract diagnoses, and we discuss a practical way to test it.

Moreover, all of the of a system and, after detection, to determine the location faults that occurred within the (possibly extended) time interval and/or the type of system faults that caused the abnormal during which the system has been observed must be behaviour. A diagnosis hypothesis indicates which fault(s) accounted for in the diagnosis. Considering again the diagnosis occurred in the system, and the diagnosis is the set of alternative of a car, for each component we could be interested hypotheses that explain (i.e., are compatible) with in knowing whether a fault has occurred to it during the last the observed system behaviour. In this paper, we focus on week; in such a case, it is difficult to perform a drastic abstraction Model-Based Diagnosis (MBD) of Discrete-Event Systems of the model without losing any precision in the (DESs, see (Cassandras and Lafortune 1999)), where the diagnosis discrimination among different hypotheses. is computed by comparing a complete DES model In this article, we study a novel approach to reduce the of the system behaviour with a (partial) observation of the complexity of DES diagnosis, based on a reformulation of actual system behaviour (Sampath et al. 1995).

We report the results obtained during the verification of Autosub6000, an autonomous underwater vehicle used for deep oceanic exploration. Our starting point is the Simulink/Matlab engineering model of the submarine, which is discretised by a compiler into a representation suitable for model checking. We assess the ability of the vehicle to function under degraded conditions by injecting faults automatically into the discretised model. The resulting system is analysed by means of the model checker MCMAS, and conclusions are drawn on the system's ability to withstand faults and to perform self-diagnosis and recovery. We present lessons learnt from this and suggest a general method for verifying autonomous vehicles.

This article contains an overview of recent and ongoing projects at Boeing's Huntsville Advanced Computing Group (ACG). In addition, it contains an overview of some of the work being conducted by Boeing's Advanced Civil Space Systems Group. One aspect of ACG's charter is to support the efforts of other groups at Boeing. Thus, AI is not considered a stand-alone field but, instead, is considered an area that can be used to find both long- and short-term solutions for Boeing and its customers. All the projects listed here represent a team effort on the part of both ACG researchers and members of other Boeing organizations.