Engineering topics
Publications and source records attributed to Aaron Dutle.
Creating formally verified implementations of software can be time-consuming and difficult. This presentation details this process, and the attempts at easing the level of difficulty and human interaction. It begins by discussing the verification of an implementation of the Compact Position Reporting algorithm, which was an involved and manual process, and goes on to show the advances made since.
DANTi is a prototype Electronic Flight Bag which incorporates an assistive Detect and Avoid (DAA) capability developed by NASA.
Explore the source record for details and available documents.
Explore the source record for details and available documents.
Requirements specification and analysis is widely applied to ensure the correctness of industrial systems in safety critical domains. Requirements are often initially written in natural language, which is highly ambiguous, and as a second step transformed into a language with rigorous semantics for formal analysis. [Question/problem] In this paper, we report on our experience in requirements creation and analysis, as well as run-time monitor generation using the Formal Requirement Elicitation Tool (FRET), on an industrial case study for a Lift-Plus-Cruise concept aircraft. [Principal ideas/results] We study the creation of requirements directly in the structured language of FRET without a prior definition of the same requirements in natural language. We focus on requirements describing state machines and discuss the challenges that we faced, in terms of creating requirements and generating monitors. We demonstrate how realizability, i.e., checking whether a requirements specification can be implemented, is crucial for understanding temporal interdependencies among requirements. [Contribution] Our study is the first complete attempt at using FRET to create industrial, realizable requirements and generate run-time monitors. Insight from lessons learned was materialized into new features in the FRET and JKind analysis frameworks.
This paper presents an interpretation and mathematical definition of the right-of-way rules as stated in USA, Title 14 of the Code of Federal Regulations, Part 91, Section 91.113 (14 CFR 91.113). In an encounter between two aircraft, the right-of-way rules defines which aircraft, if any, has the right-of-way and which AQ2 aircraft must maneuver to stay well clear of the other aircraft. The objective of the work presented in this paper is to give an unambiguous interpretation of the rules. From the interpretation, a precise mathematical formulation is created that can be used for analysis and proof of properties. The mathematical formulation has been defined in the Prototype Verification System (PVS) and properties of well formedness and core properties of the formalization have been mechanically proved. This mathematical formulation can be implemented digitally, so that right-of-way rules can be used in simulation or in future autonomous operations.
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.
Requirements specification and analysis is widely applied to ensure the correctness of industrial systems in safety critical domains. Requirements are often initially written in natural language, which is highly ambiguous, and as a second step transformed into a language with rigorous semantics for formal analysis. In this paper, we report on our experience in requirements creation and analysis, as well as run-time monitor generation using the Formal Requirement Elicitation Tool (FRET), on an industrial case study for a Lift-Plus-Cruise concept aircraft. We study the creation of requirements directly in the structured language of FRET without a prior definition of the same requirements in natural language. We focus on requirements describing state machines and discuss the challenges that we faced, in terms of creating requirements and generating monitors. We demonstrate how realizability, i.e., checking whether a requirements specification can be implemented, is crucial for understanding temporal interdependencies among requirements. Our study is the first complete attempt at using FRET to create industrial, realizable requirements and generate run-time monitors. Insight from lessons learned was materialized into new features in the FRET and JKind analysis frameworks.
Runtime assurance is a control framework where a complex controller operates under the observation of a monitor. If the monitor detects the controller exhibiting undesirable behavior, control is passed off to a trusted controller until a desirable state is regained. The runtime assurance architecture provides a layer of assurance to the system being controlled, but special care must be taken that the resulting overall system, consisting of the monitors and controllers, is behaving as intended. This talk aims to formally model and reason about runtime assurance-equipped systems as hybrid programs- which are models that consist of both discrete and continuous components. Using the verification tool Plaidypvs, safety properties of some examples involving RTA architectures is shown.
Explore the source record for details and available documents.
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, allowing 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.
The safety- and mission-critical nature of much of the work done at NASA requires algorithms and software to be exceedingly reliable. Formal methods techniques are one way of ensuring this high level of robustness. This talk will discuss the development and formal verification of autonomous aircraft path planning algorithms related to the Bellman-Ford shortest path algorithm, including consideration of distributed computation of the algorithm.
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, allowing 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.
This paper describes the formal verification of one of the most well-known algorithms for finding the shortest path between all vertices in a directed graph, namely the Bellman-Ford algorithm. This formal verification, performed in the Prototype Verification System (PVS), is motivated by two applications in the aerospace domain which use the algorithm for path planning. The first is a pre-flight calculation that uses an adapted version of Bellman-Ford to find a route intended to maximize GNSS availability throughout the flight. The second is a more traditional application intended to find the shortest path between an autonomous aircraft's current position and a goal waypoint, while avoiding regions of space specified by geofences. A novel aspect of this formal verification effort is the inclusion of two distinct models of computation for the algorithm, one being a traditional serial computation, and the other being an explicitly parallel computation. The ability to use parallel computation in the Bellman-Ford algorithm is in fact why it was chosen over other traditionally more performant algorithms, especially for the GNSS application, where the size of the graph makes a purely serial computation infeasible.
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 hand control of the overall system to a trusted controller when an untrusted one 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. 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. In the simplex RTA framework, a system has an advanced controller (AC) and a reversionary controller (RC). The system is allowed to operate with the AC until a runtime monitor detects that some property has been violated and then the RC takes over. Assuming that the sample rate of the monitor will detect improper functioning with enough time for the RC to correct the impending problem, and that the RC is trusted, the system will operate as intended. This use of the simplex RTA framework can allow for the integration of untrusted, but possibly more performant, controllers in a safe way. This paper presents a formalization of a simplex RTA framework in the Prototype Verification System (PVS) theorem prover using an embedding of differential dynamic logic (DDL) called Plaidypvs. A novel feature of this framework is that it can be instantiated at different levels of abstraction. This feature allows for the formal verification of a system with an untrusted black box component, such as an AI/ML controller. This paper does not address the many difficulties in deploying RTA in an industrial-level system. Instead, the focus is on the formal verification of the simplex RTA framework in the language of hybrid programs. 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. A selection of Unmanned Aircraft Systems (UAS) operations are shown as instances of the general RTA framework in PVS. This 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.
Explore the source record for details and available documents.
This is an overview of some of the successes of the Formal Methods team at NASA Langley. It includes discussion of the development of the Well-Clear definition for uncrewed aircraft and the subsequent creation of the DAIDALUS Detect and Avoid library, followed by discussion of the team's verification of the Compact Position Reporting algorithm, which led to the development of tools for floating-point analysis.