The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality that allow for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors.These kinds of systems arise in many safety-and mission-critical applications.This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus.The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself.This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs.The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.

This paper presents DANTi, a research tool that supports the development of Assistive Detect and Avoid (ADAA) for General Aviation. ADAA is a future on-board aircraft technology intended to augment the pilots' see-and-avoid capabilities by helping them identify and resolve traffic conflicts earlier and more efficiently. DANTi includes a realistic Electronic Flight Bag display, which provides alerts and maneuver guidance using a highly-configurable detect and avoid (DAA) library, and a fast-time simulation environment that can be fully customized to meet different research requirements. As part of NASA research efforts, DANTi is used in the Air Mobility Pathfinders project on future air transportation systems and in a joint NASA/FAA Laboratory Integrated Test Environment (NFLITE) on next-generation airspace operations in urban environments. These efforts investigate ADAA requirements in advanced urban air mobility settings where new aircraft types, new services, and new traffic patterns will be integrated in an overall crowded airspace. This paper describes the design and capabilities of DANTi, as well as use cases demonstrating some of the current research activities enabled by the tool. DANTi is freely available under NASA's Open Source Agreement.

Assistive DAA refers to the use of DAA technology in onboard-piloted aircraft to augment pilots' see-and-avoid abilities and thus enhance the safety and efficiency of visual flight operations. ADAA is anticipated to be safety-enhancing in airspace where traffic density is high or traditional air traffic services are limited, such as in future Urban Air Mobility (UAM) environments. UAM concepts under development by the FAA, NASA, and industry focus on moving people and cargo in urban and suburban areas using innovative technologies, operations, and aircraft, including electric vertical takeoff and landing (eVTOL) aircraft. Researchers at NASA, in collaboration with FAA researchers, have conducted a series of medium-fidelity, human-in-the-loop research simulations of potential future UAM operations. These simulations have included use of a NASA-developed ADAA research tool called DANTi. This paper reports on experience and observations made during testing of the DANTi ADAA capability in a simulation environment for UAM operations.

Small round-off errors in safety-critical systems can lead to catastrophic consequences. In this context, determining if the result computed by a floating-point program is accurate enough with respect to its ideal real-number counterpart is essential. This paper presents PRECiSA 4.0, a tool that rigorously estimates the accumulated round-off error of a floating-point program. PRECiSA 4.0 combines static analysis, optimization techniques, and theorem proving to provide a modular approach for computing a provably correct round-off error estimation. PRECiSA 4.0 adds several features to previous versions of the tool that enhance its applicability and performance. These features include support for data collections such as lists, records, and tuples; support for recursion schemas; an updated floating-point formalization that closely characterizes the IEEE-754 standard; an efficient and modular analysis of function calls that improves the performances for large programs; and a new user interface integrated into Visual Studio Code.

Runtime Assurance (RTA) is a design-time architecture for safety-critical systems where an internal monitor acts upon detecting a violation of a property. The simplex architecture is an instance of RTA, where the action taken is to give control of the overall system to a trusted controller when an untrusted controller violates a safety property. Simplex RTA is emerging as a method for allowing AI/ML and other unverified software to be integrated into safety-critical applications like aircraft operations. To this end, the American Society for Testing and Materials (ASTM) and NASA have each published guidelines on the use of RTA in such systems. A formal verification of the simplex RTA framework in the language of hybrid programs is extended in this work. Hybrid programs are programs that include both discrete and continuous dynamics and can be used to model complex cyber-physical systems. Plaidypvs is a tool that enables formalization of hybrid programs in the PVS theorem prover. Plaidypvs enables the verification of the general simplex RTA framework and then, by specializing some components of the hybrid program, verifying instances of the framework while treating the untrusted component as a black box. This paper presents the application of this formalization to a selection of Unmanned Aircraft Systems (UAS) operations. The formal verification process offers the benefit of design time verification of relevant safety properties to the system, and it also gives requirements on the sample rate of sensors that determine the time interval in which the ‘switch’ property of the RTA framework is checked.

Differential temporal dynamic logic dTL(2) is a logic to specify and verify temporal properties of hybrid systems. It extends differential dynamic logic (dL) with temporal operators that enable reasoning on intermediate states in both discrete and continuous dynamics. This paper presents an embedding of dTL(2) in the Prototype Verification System (PVS). The embedding includes the formalization of a trace semantics as well as the logic and proof calculus of dTL(2), which have been enhanced to support the verification of universally quantified reachability properties. The embedding is fully functional and can be used to interactively verify hybrid programs in PVS using a combination of PVS proof commands and specialized proof strategies.

The presence of round-off errors in floating-point programs may provoke a significant divergence between the actual result of the computation and the one ideally obtained using exact real-number arithmetic. These rounding errors are particularly problematic in the context of safety-critical systems such as aerospace applications. In fact, in this context, even a small rounding error can lead to catastrophic consequences when not appropriately accounted for. This paper shows how different formal methods tools can be combined to perform rigorous round-off error analysis of avionics software and outlines the challenges and the open problems in this field. Three case studies taken from real-world avionics applications are presented: the ADS-B Compact Position Reporting Algorithm, the winding number point-in-polygon algorithm used for geofencing of unmanned vehicles, and a function from the NASA DAIDALUS suite of detect-and-avoid solutions developed by NASA.

This paper presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs.

A semantic embedding is a logical encoding of a formal language, namely the object language, into the specification language of a logical framework. In their seminal paper “Experience with embedding hardware description languages in HOL”, Boulton et al. coined the terms deep and shallow embeddings depending on whether or not the syntax of terms of the target language is represented by a data type in the specification language. Thus, a deep embedding enables reasoning about classes of terms, while a shallow embedding limits reasoning to concrete terms. Embeddings of programming languages are well-known applications of interactive theorem provers, specially of those based on higher-order logic. These embeddings are often intended to support the study of a programming language semantics or to enhance a programming language with the deductive capabilities of the logical framework. A different type of embeddings, here referred to as structural embeddings, are intended to augment specification languages with structural elements of the object language. In a structural embedding, the outermost elements of the object language, i.e., the structural parts, are encoded, either deeply or shallowly, but the internal elements, i.e., the basic expressions, are those of the specification language. Advances in automated reasoning and user interfaces have enabled structural embeddings to enhance usability of interactive theorem provers and to reduce the gap between verification tools and modeling tools used by practitioners. This talk presents an overview of several years of research on theorem proving in safety-critical aerospace systems through the lens of embeddings and, more particularly, structural embeddings. The talk focuses on lessons learned and provides examples of successful applications to automated reasoning, termination analysis, floating-point analysis, and verification of cyber-physical systems. Our main point, which is hardly original, is that interactive theorem provers will serve as intermediate systems that connect a cluster of components. Structural embeddings could then provide the frontend capabilities to access this cluster of components.

This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

This paper presents the Simulation Infrastructure for Research on Interoperating Unmanned Systems (SIRIUS), a research framework for simulation and analysis of future conceptual Urban Air Mobility (UAM) operations. SIRIUS is being developed under the auspices of the NASA Air Traffic Management eXploration project, UAM subproject (ATM-X UAM). SIRIUS provides an intuitive, highly configurable graphical user interface to design complex traffic scenarios and airspace configurations representative of conceptual UAM operations. Aircraft simulated with SIRIUS can be equipped with flight-tested capabilities for detect and avoid (DAA), geofencing, distributed merging and spacing, path conformance, and path planning while executing time-constrained, 4D trajectories generated by a UAM ground operations system. Central to the design of the SIRIUS simulation framework is the capability to evaluate the integration and interoperability of ground-based separation services (e.g., strategic separation) with extended DAA functionality (e.g., path monitoring, separation provision, merging and spacing, etc.) The simulation environment also supports modelling of wind, navigation, and sensor uncertainties, as well as communication delays. SIRIUS enables distributed simulation of large-scale scenarios. An interactive graphical analysis capability helps isolate, visualize, and compare relevant vehicle state data and widely used measures of performance metrics across multiple scenarios.

This paper describes a proof-of-concept mission demonstrating a multi-agent system performing visual inspection of damage sustained by a spacecraft. Free-flying satellites, simulated by unmanned aerial vehicles (UAVs), autonomously fly around a mock space module maximizing the search space for damage detection. The free-flyers are responsible for independently coordinating their flights to avoid collision with the space module and each other, while executing mission tasks. Damage analysis on the surface of the mock space module is performed in real-time using video from each free-flyer. Three-dimensional modeling is deployed offline to supplement and improve damage detection. This approach demonstrates the feasibility of deploying real space systems for damage detection, where 2D analysis can quickly determine region of interest and 3D visualization can produce a human-navigable virtual environment with depth perspective for further investigation.

This paper presents a strategy for verifying that an aircraft following a polynomial path complies with a given set of safety criteria in continuous time. Such criteria ensure that a minimal separation between the aircraft and a set of obstacles, which can be either static or dynamic, is maintained. Dynamic obstacles are also assumed to follow a known polynomial path. Dynamic obstacles may, for example, correspond to a separation volume around another flying aircraft. In the most general case, the separation criteria vary in time depending upon the position and relative velocity between the aircraft and the obstacle. The efficiency and scalability of the proposed algorithm, to be called PolySafe, make it suitable for real-time conflict detection and path re-planning of aircraft flying in a complex and crowded airspace. PolySafe has been formally verified to guarantee the detection of conflicts within a finite time horizon.

The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate current state information, including position and velocity messages, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B protocol responsible for the encoding and decoding of aircraft positions. CPR is sensitive to computer arithmetic since it relies on functions that are intrinsically unstable such as floor and modulus. In this paper, a formal verification of the CPR algorithm is presented. In contrast to previous work, the algorithm presented here encompasses the entire range of message types supported by ADS-B. The paper also presents two implementations of the CPR algorithm, one in double-precision floating-point and one in 32-bit unsigned integers, which are both formally verified against the real-number algorithm. The verification proceeds in three steps. For each implementation, a version of CPR, which is simplified and manipulated to reduce numerical instability and leverage features of the datatypes, is proposed. Then, the Prototype Verification System (PVS) is used to formally prove real conformance properties, which assert that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify software conformance properties, which say that the software implementation of the improved algorithm is correct with respect to its idealized real-number counterpart. In concert, the two properties guarantee that the implementation meets the original specification. The two implementations will be included in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.

This paper presents a distributed consensus algorithm for autonomous merging and spacing that enables unmanned aircraft systems (UAS) to coordinate their passage through an aerial intersection (i.e., merging fix) via a distributed control mechanism. The algorithm is incorporated into the Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS). In-trail spacing between aircraft is achieved with the integration of sense and avoid functionality (SAA) within the ICAROUS framework. This approach allows vehicles to maintain required spacing while entering or exiting the merging fix. Enabling autonomously coordinating vehicles in merging and spacing operations is a key capability in facilitating vehicle traffic in urban airspace and air-mobility operations involving small UAS and other Electrical-Vertical Takeoff/Landing (E-VTOL) vehicles.

Detect and Avoid (DAA) systems are safety enhancement software applications that provide situational awareness and maneuvering guidance to aid aircraft pilots in avoiding and remaining well clear from other aircraft in the airspace. This paper presents a graphical toolkit, called DAA-Displays, designed to facilitate the assessment of compliance of DAA software implementations to formally specified functional and operational requirements. The toolkit integrates simulation and prototyping technologies allowing designers, domain experts, and pilots to compare the behavior of a DAA implementation against its formal specification. The toolkit has been used to validate an actual software implementation of DAA for unmanned aircraft systems against a standard reference algorithm that has been formally verified.

NASA's UAS Traffic Management (UTM) concept proposes a federated, service-based traffic management system for small UAS operating at altitudes below 400 feet. Under this concept, private entities operate UTM Service Suppliers (USS) and are responsible for approval, coordination, and deconfliction of flight plans submitted by mission operators. Due to unforeseen factors, any number of off-nominal conditions could force a participating vehicle to stray from the approved flight plan and become non-conforming. NASA Langley Research Center (LaRC) conducted a series of flight tests referred to as Pathfinder 1 to demonstrate the use of onboard autonomy-enabling technologies in scenarios where a non-conforming UAS flies through the assigned airspace of another vehicle while trying to reach an emergency landing site. Two test vehicles were equipped with an onboard autonomy software developed at NASA LaRC referred to as ICAROUS (Independent Configurable Architecture for Reliable Operation of Unmanned Systems). ICAROUS's autonomous sense and avoid (SAA) and geofence conformance capabilities were tested and demonstrated in the Pathfinder 1 flight tests. In these flight tests, the two aircraft initially follow flight plans that have been previously approved by a USS and determined to be conflict-free. During the flight, a scripted emergency scenario is triggered, requiring one vehicle to make an emergency landing using an onboard application named Safe2Ditch to select the best landing site. A straight-line path to the landing site would cause the UAS to become non-conforming and cross directly through the airspace of the other UAS, creating an elevated risk of collision. Two methods of autonomous onboard conflict resolution were tested to resolve this scenario and prevent collision. In the first method, the non-conforming vehicle flew directly to the landing site, passing through the airspace of the conforming vehicle. The conforming vehicle used ICAROUS's SAA capability to autonomously deviate from its flight plan to maintain a well-clear distance of 500 feet then returned to the flight plan once the conflict had passed. In the second resolution method, a keep-out geofence was placed 500 feet around the flight plan of the conforming vehicle. The non-conforming vehicle used ICAROUS to plan a route to the landing site that respected the geofence and thus maintained a safe separation from the airspace of the conforming vehicle. This paper also reports on the use of FLARM (Flight Alarm), a vehicle-to-vehicle position communication technology that transmits on 915 MHz, to provide traffic vehicle position data for onboard SAA.

This paper reports the flight test results of an on-demand, distributed, consensus based merging algorithm for autonomous multi-agent coordination used to regulate flow of air traffic through a common intersection or merge fix in a given airspace. Distributed merging is enabled by vehicle-to-vehicle (V2V) communication technology, a distributed consensus algorithm and a scheduling algorithm to coordinate the arrival times of the vehicles approaching a merge fix. The proposed algorithm is integrated into the ICAROUS (Independent Configurable Architecture for Reliable Operations of Unmanned Systems) software suite and was used to demonstrate the merging capability in a flight test campaign. The objectives of these flight tests were to validate the distributed consensus-based merging algorithm and to evaluate the requirements and associated challenges in ensuring the successful application of the algorithm in a real-world setting. Details of the flight test setup, hardware used, impediments to the achievement of the outlined objectives, flight test results and lessons learned are documented in this paper.

Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numerical computations. Writing programs that take into consideration test instability is a difficult task that requires expertise on finite precision computations and rounding errors. This paper presents a toolchain to automatically generate and verify a provably correct test-stable floating-point program from a functional specification in real arithmetic. The input is a real-valued program written in the Prototype Verification System (PVS) specification language and the output is a transformed floating-point C program annotated with ANSI/ISO C Specification Language (ACSL) contracts. These contracts relate the floating-point program to its functional specification in real arithmetic. The transformed program detects if unstable tests may occur and, in these cases, issues a warning and terminate. An approach that combines the Frama-C analyzer, the PRECiSA round-off error estimator, and PVS is proposed to automatically verify that the generated program code is correct in the sense that, if the program terminates without a warning, it follows the same computational path as its real-valued functional specification.