Engineering Papers⌕ Search

Engineering topics

J Tanner Slagel

Publications and source records attributed to J Tanner Slagel.

18 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2024

Uncrewed Aerial Systems for Emergency Medical First Response: A Market Research Report

This report presents the findings from market research conducted for NASA’s Aerial Aid Convergent Aeronautics Solutions (CAS) exploration project, which aims to assess the current state of the market and technological readiness for Uncrewed Aerial Systems (UAS) for medical emergency first response. The research reveals a robust and rapidly growing market for UAS, with a notable emerging sector for Drones as First Responders (DFR). Despite this growth, DFR applications are currently limited by regulatory, technical, and other challenges, which restrict their use primarily to manned remote video surveillance, and therefore are primarily employed by police units. To our knowledge, there is no evidence of UAS being utilized by medical first responders for scene assessment. Limited evidence exists for closely related applications; however, these are mostly confined to pilot programs for the delivery of medical supplies or equipment. Although there has been discussion around fully autonomous DFR applications for medical purposes such as UAS ambulances or patient transport drones, these applications are generally not yet operational in practice. The technology for full autonomy, especially in guidance and control, has seen significant advancements, and recent Federal Aviation Administration (FAA)regulations are likely to accelerate adoption. Computer vision algorithms for fully autonomous medical emergency response scene surveillance are primed for advancement and deployment. A notable gap likely exists between advancements in computer vision research and what is being integrated in the commercial DFR sector. This gap is primarily due to challenges such as quality assurance for autonomous systems, the availability of application-specific training datasets for computer vision algorithms, regulatory constraints, and public perception and privacy concerns.

Joshua M Fody↗
NASA NTRS2022

NASA System-Wide Safety Wildland Firefighting Operations Workshop Report

On March 9-11, 2022, NASA’s System-Wide Safety Wildland Firefighting Operations Workshop engaged the broader wildland firefighting management ecosystem in a safety-oriented discussion via a virtual platform. This enabled a better understanding of how NASA and community expertise can be leveraged in the safe development of current and future firefighting systems and operations. The goals of the workshop were to: (1) identify and prioritize the top safety-oriented risks, gaps in capabilities, and emerging technologies to enhance wildland firefighting for both near-term and far-term concepts, with a specific focus on aviation operations and (2) engage the stakeholder community in defining emergent safety-oriented scope, roles, responsibilities, and procedures for agents undergoing increasingly complex wildland firefighting operations in information-rich, but uncertain environments. Workshop participants were solicited from wildland firefighting stakeholders across government, industry, and academia. All levels of government were engaged, as NASA sought attendees from federal, state, local, and tribal government agencies. Industry participants from traditional wildland firefighting domains such as data visualization and equipment manufacturers were invited, and corporate attendees from novel application domains such as aerial robotics and autonomous systems were present as well. The top three findings were as follows: (1) Enhancing situation awareness is a safety priority, especially in the use of aerial assets; (2) Timely access to information along with data fusion and integrated displays will enhance safety-critical decision-making both inside and outside aviation contexts; and (3) Tailorable standards and common operating pictures in the field will enhance inter-agency cooperation in the wildland firefighting lifecycle and enable the optimal use of limited resources such as aerial assets. The workshop helped inform NASA of the relevant safety-related wildland firefighting concerns and aided the broader ecosystem in understanding the potential safety-oriented role NASA might play in this community. Increased engagement with crucial governmental stakeholders (e.g., U.S. Forest Service, CAL FIRE, etc.) along with industry partners in cutting- edge information -centric domains is a fundamental next step. Additionally, the workshop findings will help define the first of a series of operationally challenging demonstrations, held in concert with strategic ecosystem partners, known as the Safety Demonstrator Series for NASA’s System-Wide Safety project. The first demonstration is set in the wildland firefighting application domain and will: (1) examine high risk operational scenarios to reduce their overall risk via services, functions or capabilities that act as risk mitigators (or transfer that risk to automated systems better able to tolerate it) and (2) explore novel tools and technologies that will enhance safety margins by enabling non-traditional or neoteric operational paradigms.

wildland firefighting↗
NASA NTRSDate not supplied

Intelligent Lemma Selection for Formal Methods Proofs

To help in formally verifying the correctness of various systems, NASA constructs mathematical proofs using the proof assistant PVS (Prototype Verification System). Throughout this effort, NASA has amassed a library of tens of thousands of proven lemmas. While these lemmas can often be applied to new problems, their abundance can make lemma selection a non-trivial task. This project focuses on creating a lemma selector for use in PVS based on existing systems MePo, MaSh, and MeSh, which were written for other proof assistants. An initial benchmark system makes selections based on symbol-level similarity while the final lemma selector is a hybrid system, combining the classical approach used in the benchmark with a machine learning approach which leverages the lemmas' past usage.

Connor T Baumler↗
NASA NTRSDate not supplied

Formal Verification of the Interaction Between Semi-Algebraic Sets and Real Analytic Functions

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts interact in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predicable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The favorable way that a real analytic function enters and exits a semi-algebraic set is proven. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, these favorable interactions with semi-algebraic sets may fail.

Real analytic functions↗
NASA NTRSDate not supplied

Towards Formalization of Advanced Linear Algebra with Applications to Dynamical Systems using PVS

Linear Algebra is essential for numerous aerospace problems of interest. Formal reasoning about hybrid systems that contain variables modeled by differential equations rely on concepts from Linear Algebra such as eigenvalues, matrix decompositions, and matrix valued functions. For example, the long-term dynamics of a system of differential equations depend on the stability/instability of its equilibrium points, which often reduces to an eigenvalue problem. This talk will embark on a quest to formalize theorems and results about eigenvalues and eigenvectors using PVS. We shall start our journey with 2 x 2 complex matrices, where we will apply our PVS code to a simple example of a dynamical system. Since it can be difficult or impossible to give simple expressions of eigenvalues for larger matrices (i.e. 5 x 5 or higher), we then move towards specifying the power method for verified computation of eigenvalue approximations in PVS. This effort requires development of multivariate complex arithmetic. At the end of the day, having such additions to the PVS NASA libraries will help move towards the use of formal methods to verify concepts of control theory and system level verification.

Linear Algebra↗
NASA NTRSDate not supplied

Matrix Theory for Data Association in PVS

Consider a collection of data generated by sensors from a set of aircraft. Data association is the process of connecting each sensor measurement with its corresponding aircraft. Furthermore once the data association has taken place, the state of the aircraft can be approximated using a Kalman filter. This talk aims to explore formal specification and verification of data association in the Prototype Verification System (PVS). Formal specification and verification of data association includes development of Kalman filters, Mahalanobis distance, and other topics of matrix analysis in PVS.

Linear Algebra↗
NASA NTRSDate not supplied

Applying Formal Methods to Safety-Critical Systems

How do you know a proof is correct? Traditionally, mathematical proofs are socially verified – at least one human, following a set of implicit rules of natural language and logic, determines if the proof is believable. If the proof becomes overly tedious and/or is essential to some safety- or mission-critical application, it becomes necessary to determine the soundness to a higher standard. 'Formal methods' refer to mathematically rigorous techniques and tools that enable specification, design, and verification of hardware and software systems. The specification used in formal methods are statements in a mathematical logic while the formal verifications are deductions in that logic. Formal methods can be difficult or time/resource intensive, but offer a higher level of assurance than standard verification through testing or handwritten proofs. This talk will introduce formal methods, motivated by applications of interest to NASA, including uncrewed aircraft operations in the national airspace, urban air environments, and wildfire areas. The audience will be given a crash course in mechanically verified proofs in the Prototype Verification System (PVS), an interactive theorem prover.

Formal Methods↗
NASA NTRSDate not supplied

Formalized Reasoning of Operational Volumes for Wildland Fire Fighting

This work is focused on the formalized reasoning of operational volumes as it relates to the current and future technologies developed by NASA to aid in wildfire fighting operations. One such technology is the unmanned aircraft system pilot kit (UASP-kit) developed by the Scalable Traffic Management for Emergency Response Operations (STEReO) project at NASA, which is used to increase situation awareness for a ground operator in the field. The UASP-kit utilizes operational volumes which represent mission areas and alerting volumes, to alert when another aircraft is within one of these volumes from received ADS-B data. This work is focused on developing a rigorous foundation for the concept of operational volumes for modeling and prototyping operations in such a tool as the UASP-kit. This includes establishing a class of algorithms to detect when an object is in an operational volume, and when an operational volume is intersecting or contained within another. Additionally, this work is focused on providing rigorous proof in an interactive theorem prover that the algorithms work as intended. Scenarios are presented that model current UASP-kit operations and extend past the current capabilities of the technology to modeling more complex scenarios such as mission planning.

Operational Volumes↗
NASA NTRSDate not supplied

Formalized Reasoning of Operational Volumes for Wildland Fire Fighting

This work is focused on the formalized reasoning of operational volumes as it relates to the current and future technologies developed by NASA to aid in wildland firefighting operations. One such technology is the Unmanned Aircraft System Pilot Kit (UASP-kit) developed by the Scalable Traffic Management for Emergency Response Operations (STEReO) project at NASA, which is used to increase situational awareness for a ground operator in the field. The UASP-kit utilizes operational volumes to represent mission areas and alerting volumes; these volumes, in combinations with ADS-B data, can then be used to alert the ground operator when another aircraft has entered one of these areas. This work presents a rigorous foundation for the concept of operational volumes for modeling and prototyping operations in such a tool as the UASP-kit. This includes establishing a class of algorithms to detect when an object is in an operational volume, and when one operational volume intersects or is contained in another. Additionally, this work provides rigorous proof that the algorithms work as intended. Scenarios are presented that model current UASP-kit operations and extend past the current capabilities of the technology to modeling more complex scenarios such as mission planning.

Operational Volumes↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

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.

Runtime assurance↗
NASA NTRSDate not supplied

Ongoing Work: A Prototype Dataset for Low-flying Autonomous Medical UAS Operations

This paper presents ongoing work to create a dataset for low-flying autonomous medical UAS operations, focused on human stance recognition. This is an exploration of the viability of airborne classification for the Drone as a First Responder (DFR) concept in which a UAS arrives at the scene of an incident before emergency response personnel can get there and provides some level of situational awareness for the personnel arriving to the scene. Future incarnations could also see the UAS administer some level of care to injured parties at the scene. The data set, focused on detecting human stance, being developed here is the result of 30 test flights at NASA Langley Research Center in early 2024. In addition to flights where the participant (an anthropomorphic testing device or human) is alone in the viewing area holding a particular stance, two emergency scenes have been fabricated and collected through video - ``bike crash'' and ``difficult camping''. These test flights include four human participants. The contribution of this work upon completion will be a publicly available data set for the development of classification engines focused on human stance, and in the future, even triage.

Uncrewed Aerial Systems↗
NASA NTRSDate not supplied

A Verification Framework for Runtime Assurance of Autonomous UAS

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.

PVS↗