Engineering topics

Munoz, Cesar A.

Publications and source records attributed to Munoz, Cesar A..

At least 19 records

NASA NTRS2019

Provably Correct Floating-Point Implementation of a Point-In-Polygon Algorithm

The problem of determining whether or not a point lies inside a given polygon occurs in many applications. In air traffic management concepts, a correct solution to the point-in-polygon problem is critical to geofencing systems for Unmanned Aerial Vehicles and in weather avoidance applications. Many mathematical methods can be used to solve the point-in-polygon problem. Unfortunately, a straightforward floating- point implementation of these methods can lead to incorrect results due to round-off errors. In particular, these errors may cause the control flow of the program to diverge with respect to the ideal real-number algorithm. This divergence potentially results in an incorrect point-in- polygon determination even when the point is far from the edges of the polygon. This paper presents a provably correct implementation of a point-in-polygon method that is based on the computation of the winding number. This implementation is mechanically generated from a source- to-source transformation of the ideal real-number specification of the algorithm. The correctness of this implementation is formally verified within the Frama-C analyzer, where the proof obligations are discharged using the Prototype Verification System (PVS).

Moscato, Mariano M.↗

NASA NTRS2019

A Learning-Based Guidance Selection Mechanism for a Formally Verified Sense and Avoid Algorithm

This paper describes a learning-based strategy for selecting conflict avoidance maneuvers for autonomous unmanned aircraft systems. The selected maneuvers are provided by a formally verified algorithm and they are guaranteed to solve any impending conflict under general assumptions about aircraft dynamics. The decision-making logic that selects the appropriate maneuvers is encoded in a stochastic policy encapsulated as a neural network. The network’s parameters are optimized to maximize a reward function. The reward function penalizes loss of separation with other aircraft while rewarding resolutions that result in minimum excursions from the nominal flight plan. This paper provides a description of the technique and presents preliminary simulation results.

Balachandran, Swee↗

NASA NTRS2019

A Mixed Real and Floating-Point Solver

Reasoning about mixed real and floating-point constraints is essential for developing accurate analysis tools for floating-point pro- grams. This paper presents FPRoCK, a prototype tool for solving mixed real and floating-point formulas. FPRoCK transforms a mixed formula into an equisatisfiable one over the reals. This formula is then solved using an off-the-shelf SMT solver. FPRoCK is also integrated with the PRECiSA static analyzer, which computes a sound estimation of the round-off error of a floating-point program. It is used to detect infeasible computational paths, thereby improving the accuracy of PRECiSA.

Salvia, Rocco↗

NASA NTRS2018

Independent Configurable Architecture for Reliable Operation of Unmanned Systems with Distributed Onboard Services

This paper presents the development of ICAROUS-2 (Independent Configurable Architecture for Reliable Operation of Unmanned Systems with Distributed Onboard Services), the second generation of a software architecture that integrates several algorithms as distributed onboard services to enable robust autonomous UAS applications. In particular, the ICAROUS architecture defines a framework to perform detect and avoid, geofencing, path monitoring, path planning, and autonomous decision making to ensure safety and mission progress. Most of the core algorithms implemented in ICAROUS are formally verified using an interactive theorem prover. These algorithms are composed together using a plan execution engine, whose operational semantics is formally specified. A description of the integrated architecture, services currently available, and flight test results highlighting the capability of ICAROUS are presented.

Balachandran, Swee↗

NASA NTRS2018

An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs

This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors.

Titolo, Laura↗

NASA NTRS2017

Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis

This paper introduces a static analysis technique for computing formally verified round-off error bounds of floating-point functional expressions. The technique is based on a denotational semantics that computes a symbolic estimation of floating-point round-o errors along with a proof certificate that ensures its correctness. The symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. The proposed technique is implemented in the prototype research tool PRECiSA (Program Round-o Error Certifier via Static Analysis) and used in the verification of floating-point programs of interest to NASA.

Moscato, Mariano↗

NASA NTRS2017

Implicitly Coordinated Detect and Avoid Capability for Safe Autonomous Operation of Small UAS

As the airspace becomes increasingly shared by autonomous small Unmanned Aerial Systems (UAS), there would be a pressing need for coordination strategies so that aircraft can safely and independently maneuver around obstacles, geofences, and traffic aircraft. Explicitly coordinating resolution strategies for small UAS would require additional components such as a reliable vehicle-to-vehicle communication infrastructure and standardized protocols for information exchange that could significantly increase the cost of deploying small UAS in a shared airspace. This paper explores a novel approach that enables multiple aircraft to implicitly coordinate their resolution maneuvers. By requiring all aircraft to execute the proposed approach deterministically, it is possible for all of them to implicitly agree on the region of airspace each will be occupying in a given time interval. The proposed approach lends itself to the construction of a suitable feedback mechanism that enables the real-time execution of an implicitly conflict-free path in a closed-loop manner dealing with uncertainties in aircraft speed. If a network infrastructure is available, the proposed approach can also exploit the benefits of explicit information.

Balachandran, Swee↗

NASA NTRS2017

The MINERVA Software Development Process

This paper presents a software development process for safety-critical software components of cyber-physical systems. The process is called MINERVA, which stands for Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms. The process relies on formal methods for rigorously validating code against its requirements. The software development process uses: (1) a formal specification language for describing the algorithms and their functional requirements, (2) an interactive theorem prover for formally verifying the correctness of the algorithms, (3) test cases that stress the code, and (4) numerical evaluation on these test cases of both the algorithm specifications and their implementations in code. The MINERVA process is illustrated in this paper with an application to geo-containment algorithms for unmanned aircraft systems. These algorithms ensure that the position of an aircraft never leaves a predetermined polygon region and provide recovery maneuvers when the region is inadvertently exited.

Narkawicz, Anthony↗

NASA NTRS2017

Unmanned Aircraft Systems Minimum Operations Performance Standards End-to-End Verification and Validation (E2-V2) Simulation

As Unmanned Aircraft Systems (UAS) make their way to mainstream aviation operations within the National Airspace System (NAS), research efforts are underway to develop a safe and effective environment for their integration into the NAS. Detect and Avoid (DAA) systems are required to account for the lack of "eyes in the sky" due to having no human on-board the aircraft. The current NAS relies on pilot's vigilance and judgement to remain Well Clear (CFR 14 91.113) of other aircraft. RTCA SC-228 has defined DAA Well Clear (DAAWC) to provide a quantified Well Clear volume to allow systems to be designed and measured against. Extended research efforts have been conducted to understand and quantify system requirements needed to support a UAS pilot's ability to remain well clear of other aircraft. The efforts have included developing and testing sensor, algorithm, alerting, and display requirements. More recently, sensor uncertainty and uncertainty mitigation strategies have been evaluated. This paper discusses results and lessons learned from an End-to-End Verification and Validation (E2-V2) simulation study of a DAA system representative of RTCA SC-228's proposed Phase I DAA Minimum Operational Performance Standards (MOPS). NASA Langley Research Center (LaRC) was called upon to develop a system that evaluates a specific set of encounters, in a variety of geometries, with end-to-end DAA functionality including the use of sensor and tracker models, a sensor uncertainty mitigation model, DAA algorithmic guidance in both vertical and horizontal maneuvering, and a pilot model which maneuvers the ownship aircraft to remain well clear from intruder aircraft, having received collective input from the previous modules of the system. LaRC developed a functioning batch simulation and added a sensor/tracker model from the Federal Aviation Administration (FAA) William J. Hughes Technical Center, an in-house developed sensor uncertainty mitigation strategy, and implemented a pilot model similar to one from the Massachusetts Institute of Technology's Lincoln Laboratory (MIT/LL). The resulting simulation provides the following key parameters, among others, to evaluate the effectiveness of the MOPS DAA system: severity of loss of well clear (SLoWC), alert scoring, and number of increasing alerts (alert jitter). The technique, results, and lessons learned from a detailed examination of DAA system performance over specific test vectors and encounter cases during the simulation experiment will be presented in this paper.

Ghatas, Rania W.↗

NASA NTRS2016

Coordination Logic for Repulsive Resolution Maneuvers

This paper presents an algorithm for determining the direction an aircraft should maneuver in the event of a potential conflict with another aircraft. The algorithm is implicitly coordinated, meaning that with perfectly reliable computations and information, it will in- dependently provide directional information that is guaranteed to be coordinated without any additional information exchange or direct communication. The logic is inspired by the logic of TCAS II, the airborne system designed to reduce the risk of mid-air collisions between aircraft. TCAS II provides pilots with only vertical resolution advice, while the proposed algorithm, using a similar logic, provides implicitly coordinated vertical and horizontal directional advice.

Narkawicz, Anthony J.↗

NASA NTRS2016

Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective

As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.

Munoz, Cesar A.↗

NASA NTRS2015

Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems

As the technological and operational capabilities of unmanned aircraft systems (UAS) continue to grow, so too does the need to introduce these systems into civil airspace. Unmanned Aircraft Systems Integration in the National Airspace System is a NASA research project that addresses the integration of civil UAS into non-segregated airspace operations. One of the major challenges of this integration is the lack of an onboard pilot to comply with the legal requirement that pilots see and avoid other aircraft. The need to provide an equivalent to this requirement for UAS has motivated the development of a detect and avoid (DAA) capability to provide the appropriate situational awareness and maneuver guidance in avoiding and remaining well clear of traffic aircraft. Formal methods has played a fundamental role in the development of this capability. This talk reports on the formal methods work conducted under NASA's Safe Autonomous System Operations project in support of the development of DAA for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations. The talk also discusses technical challenges in formal methods research in the context of the development and safety analysis of advanced air traffic management concepts.

Munoz, Cesar A.↗

NASA NTRS2015

Software Validation via Model Animation

This paper explores a new approach to validating software implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input values to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illustrated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system's algorithms are carried out in the Prototype Verification System (PVS). The animation tool PVSio is used to evaluate the formal models on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual software. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.

Dutle, Aaron M.↗

NASA NTRS2015

Kodiak: An Implementation Framework for Branch and Bound Algorithms

Recursive branch and bound algorithms are often used to refine and isolate solutions to several classes of global optimization problems. A rigorous computation framework for the solution of systems of equations and inequalities involving nonlinear real arithmetic over hyper-rectangular variable and parameter domains is presented. It is derived from a generic branch and bound algorithm that has been formally verified, and utilizes self-validating enclosure methods, namely interval arithmetic and, for polynomials and rational functions, Bernstein expansion. Since bounds computed by these enclosure methods are sound, this approach may be used reliably in software verification tools. Advantage is taken of the partial derivatives of the constraint functions involved in the system, firstly to reduce the branching factor by the use of bisection heuristics and secondly to permit the computation of bifurcation sets for systems of ordinary differential equations. The associated software development, Kodiak, is presented, along with examples of three different branch and bound problem types it implements.

Smith, Andrew P.↗

NASA NTRS2015

Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions

A fundamental requirement for the integration of unmanned aircraft into civil airspace is the capability of aircraft to remain well clear of each other and avoid collisions. This requirement has led to a broad recognition of the need for an unambiguous, formal definition of well clear. It is further recognized that any such definition must be interoperable with existing airborne collision avoidance systems (ACAS). A particular class of well-clear definitions uses logic checks of independent distance thresholds as well as independent time thresholds in the vertical and horizontal dimensions to determine if a well-clear violation is predicted to occur within a given time interval. Existing ACAS systems also use independent distance thresholds, however a common time threshold is used for the vertical and horizontal logic checks. The main contribution of this paper is the characterization of the effects of the decoupled vertical time threshold on a well-clear definition in terms of (1) time to well-clear violation, and (2) interoperability with existing ACAS. The paper provides governing equations for both metrics and includes simulation results to illustrate the relationships. In this paper, interoperability implies that the time of well-clear violation is strictly less than the time a resolution advisory is issued by ACAS. The encounter geometries under consideration in this paper are initially well clear and consist of constant-velocity trajectories resulting in near-mid-air collisions.

Upchurch, Jason M.↗

NASA NTRS2014

A Formally-Verified Decision Procedure for Univariate Polynomial Computation Based on Sturm's Theorem

Sturm's Theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semiopen interval. This paper presents a formalization of this theorem in the PVS theorem prover, as well as a decision procedure that checks whether a polynomial is always positive, nonnegative, nonzero, negative, or nonpositive on any input interval. The soundness and completeness of the decision procedure is proven in PVS. The procedure and its correctness properties enable the implementation of a PVS strategy for automatically proving existential and universal univariate polynomial inequalities. Since the decision procedure is formally verified in PVS, the soundness of the strategy depends solely on the internal logic of PVS rather than on an external oracle. The procedure itself uses a combination of Sturm's Theorem, an interval bisection procedure, and the fact that a polynomial with exactly one root in a bounded interval is always nonnegative on that interval if and only if it is nonnegative at both endpoints.

Narkawicz, Anthony J.↗

NASA NTRS2014

Bifurcation Analysis Using Rigorous Branch and Bound Methods

For the study of nonlinear dynamic systems, it is important to locate the equilibria and bifurcations occurring within a specified computational domain. This paper proposes a new approach for solving these problems and compares it to the numerical continuation method. The new approach is based upon branch and bound and utilizes rigorous enclosure techniques to yield outer bounding sets of both the equilibrium and local bifurcation manifolds. These sets, which comprise the union of hyper-rectangles, can be made to be as tight as desired. Sufficient conditions for the existence of equilibrium and bifurcation points taking the form of algebraic inequality constraints in the state-parameter space are used to calculate their enclosures directly. The enclosures for the bifurcation sets can be computed independently of the equilibrium manifold, and are guaranteed to contain all solutions within the computational domain. A further advantage of this method is the ability to compute a near-maximally sized hyper-rectangle of high dimension centered at a fixed parameter-state point whose elements are guaranteed to exclude all bifurcation points. This hyper-rectangle, which requires a global description of the bifurcation manifold within the computational domain, cannot be obtained otherwise. A test case, based on the dynamics of a UAV subject to uncertain center of gravity location, is used to illustrate the efficacy of the method by comparing it with numerical continuation and to evaluate its computational complexity.

Smith, Andrew P.↗

NASA NTRS2014

An Independent and Coordinated Criterion for Kinematic Aircraft Maneuvers

This paper proposes a mathematical definition of an aircraft-separation criterion for kinematic-based horizontal maneuvers. It has been formally proved that kinematic maneu- vers that satisfy the new criterion are independent and coordinated for repulsiveness, i.e., the distance at closest point of approach increases whether one or both aircraft maneuver according to the criterion. The proposed criterion is currently used in NASA's Airborne Coordinated Resolution and Detection (ACCoRD) set of tools for the design and analysis of separation assurance systems.

Narkawicz, Anthony J.↗