Engineering PapersSearch

Engineering topics

Alwyn Goodloe

Publications and source records attributed to Alwyn Goodloe.

Wildfire-fighting Use Case Requirements to Monitor

In this technical report, we provide requirements for a wildfire-fighting use-case, towards the Safety Demonstrator 1. The use case will incorporate ground and airborne assets operating in a coordinated fashion, and will comprise five activities, from detection to the execution of the initial attack. Depending on the activity and the data involved, the requirements identified may be non-probabilistic or probabilistic. In both cases, we first identify some of the requirements we wish to monitor, and then present a formalization using the language of requirements of the NASA requirements elicitation tool FRET. To formalize probabilistic requirements, we use a novel extension to FRET’s requirements language that incorporates notions of probability, and discuss how requirements can be translated into existing probabilistic temporal logics like PCTL. We exemplify how some of the requirements presented can be monitored using the existing tools Ogma and Copilot. We close with a summary and future directions.

Requirements

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

Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors

Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (FRET), and the RV system Copilot. We extend FRET with mechanisms to capture additional information needed to generate monitors, and introduce OGMA, a new tool to bridge the gap between FRET and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our tool chain is available as open source.

FRET

Copilot 3

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. The introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. This paper presents Copilot 3, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware. This paper presents version 3 of the Copilot language, demonstrates its suitability with a number of examples, and discusses its use in larger applications. Additionally, it describes the framework?s architecture, its implementation as a Domain Specific Language (DSL) embedded in Haskell, and the progress of the project over the years.

Ivan Perez

TPSAS-NF1676L-14044-DND

The presentation will focus on the application of formal methods to safety-critical systems in aviation and space. Although the talk will mostly focus on work conducted at the NASA Langley Research Center, there will be a brief summary of work conducted at NASA?s Jet Propulsion Laboratory and Ames Research Center.

Alwyn Goodloe

TPSAS-NF1676L-15598-DND

The presentation is intended to give an overview of the verification efforts in the Safety-Critical Avionics Systems Branch at the NASA Langley Research Center. Mainly targeted at students that are interested in internships in our group.

Alwyn Goodloe

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems(ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods

Monitoring ICAROUS: From Requirements to Autonomous Flight

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods

Assuring Safety-Critical Machine Learning Enabled Systems: Challenges and Promise

Machine learning is increasingly being used in safety-critical systems, where the public safety requires a rigorous assurance process. We shall outline how assurance processes work for conventional systems and identify the primary difficulty in applying them to machine learning enabled systems. We will then outline a path forward including identifying where considerable basic research remains.

machine learning