Formal verification of industrial systems is very challenging, due to reasons ranging from scalability issues to communication difficulties with engineering-focused teams. More importantly, industrial systems are rarely designed for verification, but rather for operational needs. In this paper we present an overview of our experience using hybrid systems theorem proving to formally verify ACAS X, an airborne collision avoidance system for airliners scheduled to be operational around 2020. The methods and proof techniques presented here are an overview of the work already presented in [8], while the evaluation of ACAS X has been significantly expanded and updated to the most recent version of the system, run 13. The effort presented in this paper is an integral part of the ACAS X development and was performed in tight collaboration with the ACAS X development team.

We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using \KeYmaeraD (a tool that mechanizes QdL), we created a machine-checked proof that guarantees the new algorithm is safe for all possible inputs.

Component-based software has been proposed as a methodology for improving software reuse and has increasingly been adopted by robot software developers. At the same time, robot systems typically have real-time performance requirements and performance gains can often be obtained by multi-threading. It is challenging, however, to create correct multi-threaded software, especially when standard mutual exclusion primitives, such as mutexes and semaphores, are eschewed in favor of more efficient, lock-free mechanisms. It is even more difficult to find these errors, as they can remain dormant for years until triggered by just the “right” conditions. Our approach, therefore, is to apply Formal Methods to reason about the correctness of these mechanisms. As a first step, we adopted a recently-developed program logic called History for Local Rely/Guarantee (HLRG) and applied it to prove the correctness (after first finding and fixing an error) of one such mechanism in the open source cisst software package. This strategy is not specific to cisst and can be applied to other packages.

Density estimation is the process of taking a set of multivariate data and finding an estimate for the probability density function (pdf) that produced it. One approach for obtaining an accurate estimate of the true density f(x) is to use the polynomial-moment method with Boltzmann-Shannon entropy. Although rigorous mathematically, the method is difficult to implement in practice because the solution involves a large set of simultaneous nonlinear integral equations, one for each moment or joint moment constraint. Solutions available in the literature are generally not easily applicable to multivariate data, nor computationally efficient. In this paper, we take the functional form that was developed in this problem and apply pointwise estimates of the pdf as constraints. These pointwise estimates are transformed into basis coefficients for a set of Legendre polynomials. The procedure is mathematically similar to the multidimensional Fourier transform, although with different basis functions. We apply this technique, called the maximum-entropy density estimation (MEDE) technique, to a series of multivariate datasets.

Given an image of a scene comprised of a number of distinct terrain classes, the optimum Bayesian classifier (OBC) provides the highest possible classification accuracy of the imaged scene, provided we have a priori knowledge of the probability density function (pdf) of the sensor's output for each terrain class. If the imaging sensor consists of multiple channels, application of OBC requires knowledge of the joint pdf of the observations made by all the channels. In practice, the volume of data needed in order to generate an accurate multidimensional pdf far exceeds the size of available datasets. The data-size requirement may be relaxed by assuming the pdfs to be Gaussian in form, but such an assumption leads to suboptimum classification performance. This paper addresses the data size issue by (1) taking advantage of the maximum-entropy density estimation (MEDE) technique introduced in a companion paper and (2) using marginal pdfs in a hierarchical approach. Using multidate synthetic aperture radar observations, it was shown that the Bayesian hierarchical classifier introduced in this paper can classify short vegetation classes with an accuracy of 93%, without retraining, compared with an accuracy of 84% for the maximum-likelihood estimator (with Gaussian assumption) and only 74% with ISODATA.