Certificate functions can be used to efficiently capture and prove various properties of a system or controller. Control barrier functions (CBFs) are certificate functions that define a region of forward-invariance, which makes them a natural choice to enforce a notion of “safety” for a system. However, synthesizing CBFs, especially in the case of complex systems with learning-enabled components, remains a challenge. Recent work achieves promising results by leveraging neural networks as function approximators to learn CBFs. However, a single CBF may not exist or be difficult to obtain for complex hybrid systems. To overcome this difficulty, this paper presents a framework to simultaneously learn simpler, time-varying control barrier functions (TV-CBFs) that are composable. We embed these neural certificates in a compositional framework based on assume-guarantee contracts. The resulting neural barrier contracts can then be combined by leveraging the rigorous contract algebra. Learning multiple, composable CBFs empowers the verification process (1) by simplifying the verification of complex systems via decomposition and (2) by broadening the expressivity in capturing complex systems and controllers. We illustrate the effectiveness of our approach on the verification of an aircraft’s automatic landing system and a quadrotor navigating an indoor environment.

We survey the landscape of human operator modeling ranging from the early cognitive models developed in artificial intelligence to more recent formal task models developed for model-checking of human machine interactions. We review human performance modeling and human factors studies in the context of aviation, and models of how the pilot interacts with automation in the cockpit. The purpose of the survey is to assess the applicability of available state-of-the-art models of the human operators for the design, verification and validation of future safety-critical aviation systems that exhibit higher-level of autonomy, but still require human operators in the loop. These systems include the single-pilot aircraft and NextGen air traffic management. We discuss the gaps in existing models and propose future research to address them.

A certification process evaluates whether the risk of a system is acceptable for its intent. Certification processes are complex and usually human-driven, requiring expert evaluators to determine software conformance to certification guidelines based on a large number of development artifacts. These processes may result in superficial, biased, and long evaluations. In this paper, we propose a computer-aided assurance framework, called Automated Assurance Case Environment (AACE), enabling synthesis and validation of assurance cases (ACs) based on a system's specification, assurance evidence, and domain expert knowledge captured in AC patterns. A commercial aerospace case study shows that the generated ACs are meaningful, and numerical results show the efficiency of AACE.

Assurance cases (ACs) have gained attention in the aerospace, medical, and other heavily-regulated industries as a means for providing structured arguments on why a product is dependable (i.e., safe, secure, etc.) for its intended application. Challenges in AC construction stem from the complexity and uniqueness of the designs, the heterogeneous nature of the required supporting evidence, and the need to assess the quality of an argument. We present an automated AC generation framework that facilitates the construction, validation, and confidence assessment of ACs based on dependability argument patterns and confidence patterns capturing domain knowledge. The ACs are instantiated with a system’s specification and evaluated based on the available design and verification evidence. Aerospace case studies illustrate the framework’s effectiveness, efficiency, and scalability.

Next-generation certification processes are expected to be influenced by two dominant trends: customizable certification, as advocated by Overarching Properties (OPs), and the continuous and rapid delivery approach from the coupling of software development and operations (DevOps). In light of these trends, certification processes must adapt to support the ongoing evaluation of assurance while accommodating the emergence of new evidence and evolving safety and security practices, particularly for systems enabled by artificial intelligence (AI). These requirements call for the development of computer-aided evaluation tools that automate repetitive tasks and offer visualization aids to assist evaluators and applicants in making informed decisions. This paper aims to address the challenges associated with assurance evaluation via a survey-based analysis and proposes a user interface that streamlines the evaluation of certification arguments.

We present ARACHNE, a framework for the automated, compositional validation of assurance cases (ACs), i.e., structured arguments about the correctness or safety of a design. ARACHNE leverages assume-guarantee contracts, expressed in a stochastic logic formalism, to formally capture AC claims (guarantees) subject to their contexts (assumptions) as well as the sources of uncertainty associated with them. Given an AC, modeled as a hierarchical network of stochastic contracts, and a library of confidence models, expressed as a set of Bayesian networks, we propose a procedure that coordinates logic and Bayesian reasoning to check that the AC argument is sound and quantify its strength in terms of a confidence measure. The effectiveness of our approach is illustrated on case studies motivated by testing and validation of airborne and automotive system software.

An automatic synthesis problem is often characterized by an overall goal or specification to be satisfied, the set of all possible outcomes, called the design space, and an algorithm for the automatic selection of one or more members from the design space that are provably guaranteed to satisfy the overall specification. A key challenge in automatic synthesis is the complexity of the design space. In this paper, we introduce a formal model, termed hierarchical contract nets, and a framework for the efficient automatic synthesis of hierarchical contract nets, based on a library of refinement relations between contracts and contract nets. We show, via the application of automatic synthesis of assurances cases, that hierarchical contract-based synthesis can mitigate the design space complexity problem. We also show that the approach can bring both the benefits of automating the creation of assurance cases and ensuring that the knowledge from the argumentation experts is captured and reflected in the synthesized assurance cases.

We address the problem that state-of-the-art Convolution Neural Networks (CNN) classifiers are not invariant to small shifts. The problem can be solved by the removal of sub-sampling operations such as stride and max pooling, but at a cost of severely degraded training and test efficiency. We present a novel usage of Gaussian-Hermite basis to efficiently approximate arbitrary filters within the CNN framework to obtain translation invariance. This is shown to be invariant to small shifts, and preserves the efficiency of training. Further, to improve efficiency in memory usage as well as computational speed, we show that it is still possible to sub-sample with this approach and retain a weaker form of invariance that we call \emph{translation insensitivity}, which leads to stability with respect to shifts. We prove these claims analytically and empirically. Our analytic methods further provide a framework for understanding any architecture in terms of translation insensitivity, and provide guiding principles for design.

We investigate the topics of sensitivity and robustness in feedforward and convolutional neural networks. Combining energy landscape techniques developed in computational chemistry with tools drawn from formal methods, we produce empirical evidence indicating that networks corresponding to lower-lying minima in the optimization landscape of the learning objective tend to be more robust. The robustness estimate used is the inverse of a proposed sensitivity measure, which we define as the volume of an over-approximation of the reachable set of network outputs under all additive $l_{\infty}$-bounded perturbations on the input data. We present a novel loss function which includes a sensitivity term in addition to the traditional task-oriented and regularization terms. In our experiments on standard machine learning and computer vision datasets, we show that the proposed loss function leads to networks which reliably optimize the robustness measure as well as other related metrics of adversarial robustness without significant degradation in the classification error. Experimental results indicate that the proposed method outperforms state-of-the-art sensitivity-based learning approaches with regards to robustness to adversarial attacks. We also show that although the introduced framework does not explicitly enforce an adversarial loss, it achieves competitive overall performance relative to methods that do.

This article describes a fully automated, credible autocoding chain for control systems. The framework generates code, along with guarantees of high level functional properties which can be independently verified. It relies on domain specific knowledge and fomal methods of analysis to address a context of heightened safety requirements for critical embedded systems and ever-increasing costs of verification and validation. The platform strives to bridge the semantic gap between domain expert and code verification expert. First, a graphical dataflow language is extended with annotation symbols enabling the control engineer to express high level properties of its control law within the framework of a familiar language. An existing autocoder is enhanced to both generate the code implementing the initial design, but also to carry high level properties down to annotations at the level of the code. Finally, using customized code analysis tools, certificates are generated which guarantee the correctness of the annotations with respect to the code, and can be verified using existing static analysis tools. Only a subset of properties and controllers are handled at this point.

The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety-critical roles. There is a considerable body of mathematical proofs on on-line optimization algorithms which can be leveraged to assist in the development and verification of their implementation. In this paper, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the level of the code, thereby making it accessible for the formal methods community. The running example used in this paper is a generic semi-definite programming solver. Semi-definite programs can encode a wide variety of optimization problems and can be solved in polynomial time at a given accuracy. We describe a top-down approach that transforms a high-level analysis of the algorithm into useful code annotations. We formulate some general remarks on how such a task can be incorporated into a convex programming autocoder. We then take a first step towards the automatic verification of the optimization program by identifying key issues to be addressed in future work.

Robustness analyses play a major role in the synthesis and analysis of controllers. For control systems, robustness is a measure of the maximum tolerable model inaccuracies or perturbations that do not destabilize the system. Analyzing the robustness of a closed-loop system can be performed with multiple approaches: gain and phase margin computation for single-input single-output (SISO) linear systems, mu analysis, IQC computations, etc. However, none of these techniques consider the actual code in their analyses.The approach presented here relies on an invariant computation on the discrete system dynamics. Using semi-de finite programming (SDP) solvers, a Lyapunov-based function is synthesized that captures the vector margins of the closed-loop linear system considered. This numerical invariant expressed over the state variables of the system is compatible with code analysis and enables its validation on the code artifact.This automatic analysis extends verification techniques focused on controller implementation, addressing validation of robustness at model and code level. It has been implemented in a tool analyzing discrete SISO systems and generating over-approximations of phase and gain margins. The analysis will be integrated in our toolchain for Simulink and Lustre models autocoding and formal analysis.

Motivation 1. High software certification Cost! APPROACHING 50% OF TOTAL PROJECT development COSTS ∼ BILLIONS!) 2. MAY NOT BE practical for Certifying UNMANNED autonomous vehicles or Unmanned aerial systems

We present a domain specific process to enable the verification of observer-based fault detection software. Observer-based fault detection systems, like control systems, yield invariant properties of quadratic types. These quadratic invariants express both safety properties of the software, such as the boundedness of the states, and correctness properties, such as the absence of false alarms from the fault detector. We seek to leverage these quadratic invariants, in an automated way, for the formal verification of the fault detection software. The approach, named the credible autocoding framework, can be characterized as autocoding with proofs. The process starts with the fault detector model, along with its safety and correctness properties, all expressed formally in a synchronous modeling environment such as Simulink. The model is then transformed by a prototype credible autocoder into both code and analyzable annotations for the code. We demonstrate the credible autocoding process on a running example of an output observer fault detector for a 3 degree-of-freedom helicopter control system.

We present the usage of a prototype that is the result of our research efforts in the translation of control theory into code semantics and the automatic verification of control software using those generated semantics. We demonstrate an application of tool-chain for a jet engine, produced by the lightweight jet engine manufacturer Price Induction, running in closed-loop with its Full Authority Digital Controller (FADEC) hardware. The framework for the tool is based on the model-based development paradigm but with integration of formal methods into the development process to support the claim of correctness of the auto-generated code. The prototype is a two parts tool-chain. The credible autocoding part is designed to translate a Simulink model of a control system into an annotated C program. The annotations, which express control semantics of the system, are generated during the autocoding process and embedded into the C program as comments. The control semantics are formal expressions of the safety and performance requirements of the control system and their proofs. The second part, the verification backend, which in general runs independently of the first part, checks the correctness of the annotations with respect to the code.

A control software verification framework for gas turbine engines is developed. A stability proof is presented for gain scheduled closed-loop engine system based on global linearization and linear matrix inequality (LMI) techniques. Using convex optimization tools, a single quadratic Lyapunov function is computed for multiple linearizations near equilibrium points of the closed-loop system. With the computed stability matrices, ellipsoid invariant sets are constructed, which are used efficiently for DGEN turbofan engine control code stability analysis. Then a verifiable linear gain scheduled controller for DGEN engine is developed based on formal methods, and tested on the engine virtual test bench. Simulation results show that the developed verifiable gain scheduled controller is capable of regulating the engine in a stable fashion with proper tracking performance.

This article describes the application of a credible autocoding framework for control systems towards a nonlinear car controller example. The framework generates code, along with guarantees of high level functional properties about the code that can be independently verified. These high-level functional properties not only serves as a certificate of good system behvaior but also can be used to guarantee the absence of runtime errors. In one of our previous works, we have constructed a prototype autocoder with proofs that demonstrates this framework in a fully automatic fashion for linear and quasi-nonlinear controllers. With the nonlinear car example, we propose to further extend the prototype's dataflow annotation language environment with with several new annotation symbols to enable the expression of general predicates and dynamical systems. We demonstrate manually how the new extensions to the prototype autocoder work on the car controller using the output language Matlab. Finally, we discuss the requirements and scalability issues of the automatic analysis and verification of the documented output code.

In an effort to meet the reliability standards that control systems operating in safety-critical roles require, we have started laying the foundation for a tool-set that migrates control theory properties and proofs into the software implementation of those control systems designs. By using this tool the engineer can provide a more rigorous guarantee of the quality of the software and initiate the formal verification process. The tool focuses on control software in order to leverage the domain knowledge from existing mathematical techniques for the analysis and synthesis of control systems. As a first step in the development of the tool-set, we have created a prototype of a Scilab to C translator with proof annotation support. Though limited in its current functionalities, the development of this prototype allowed us to identify the key issues which will be used to further refine the translator. This paper describes the prototype and the further improvements planned for the translator.

We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the verification and validation of the control software. We propose extensions to a Simulink-like environment's annotation capabilities to include formal control system stability, performance properties and their proofs. We provide a conceptual description of a tool, that takes in a Simulink-like diagram of the control system as the input, and generates a graphically annotated control system diagram as the output. The annotations can either be inserted by the user or generated automatically by a third party control analysis software such as IQC$\beta$ or $\mu$-tool. We finally describe how the graphical representation of the system and its properties can be translated to annotated programs in a programming language used in verification and validation such as Lustre or C.