Search NASA⌕ Search

Engineering topics

Cesar Munoz

Publications and source records attributed to Cesar Munoz.

16 records
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

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↗
NASA NTRSDate not supplied

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↗
NASA NTRSDate not supplied

Formal Methods in the Development of Highly Assured Software for Unmanned Aircraft Systems

In traditional software development methodologies, operational and functional requirements of systems are often specified in structured natural language notations. These restricted notations provide good documentation support, but only provide limited support for semantic analysis. These notations are generally not rich enough to unambiguously specify the requirements of safety-critical systems that, for example, involve complex numerical computations or that interact with the physical environment. Examples of these safety-critical systems are autonomous vehicles such as unmanned aircraft systems. This talk advocates the use of expressive formal logics, such as higher-order logic, to specify the operational and functional requirement of unmanned systems and to prove the correctness of these requirements. Semantic analysis of requirements written in higher-order logic is supported through the use of interactive theorem provers. Formal models serve as ideal reference implementations of functional requirements. Hence, formal logics enable software validation techniques where software implementations can be checked against functional requirements in a mechanical way. The Formal Methods group in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center has conducted research on the development and application of formal verification techniques to safety-critical applications of interest to NASA for more than 30 years. This talk illustrates the use of formal methods in the development of highly-assured autonomous unmanned aircraft systems.

Formal Methods↗
NASA NTRSDate not supplied

SIRIUS: Simulation Infrastructure for Research on Interoperating Unmanned Systems

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.

Andrew Peters↗
NASA NTRSDate not supplied

Embedding Differential Dynamic Logic in PVS

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.

Formal Verification↗
NASA NTRSDate not supplied

DANTi: A Tool for Assistive Detect and Avoid Research

This paper presents DANTi, a research tool developed at NASA Langley Research Center to support the validation of Assistive Detect and Avoid (ADAA) requirements for General Aviation (GA). ADAA is a future on-board aircraft technology intended to augment a pilot’s see-and-avoid capability by helping them identify and resolve traffic conflicts earlier and more efficiently. DANTi includes a realistic Electronic Flight Bag (EFB) display and a fast-time simulation environment that can be fully customized to meet different research requirements. DANTi is currently used within NASA efforts such as the Air Mobility Pathfinders project on future air transportation systems and 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.

Detect and Avoid↗
NASA NTRSDate not supplied

Assistive Detect and Avoid Technology in Urban Air Mobility Environments

The use of Assistive Detect and Avoid (Assistive DAA or ADAA) technology in Urban Air Mobility (UAM) environments poses potential benefits as well as challenges. Assistive DAA refers to the leveraged use of DAA technology, originally developed to replace see-and-avoid capabilities for remotely piloted aircraft, in onboard-piloted aircraft to augment (rather than replace) pilots’ see-and-avoid abilities and thus enhance the safety and efficiency of visual flight operations. ADAA is anticipated to be especially safety-enhancing in airspace where traffic density is high or traditional air traffic services are limited, such as in future UAM environments. ADAA may also enable higher-tempo UAM operations than with only see-and-avoid capabilities, while still maintaining acceptable levels of safety. UAM concepts under development by the FAA, NASA, and industry focus on operations 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 Langley Research Center, in collaboration with FAA researchers at the William J. Hughes Technical Center in Atlantic City, NJ, have conducted a series of medium-fidelity, human-in-the-loop research simulations of potential future UAM operations and concepts in both Class C and Class B airspace environments. These simulations have included use of a Langley-developed ADAA research tool called DANTi, which enables configurable ADAA displays to be presented to pilots of simulated eVTOL aircraft participating in higher-density and higher-tempo UAM operations. Experience and observations made during testing of the NASA-developed DANTi ADAA capability in the UAM NFLITE simulation environment will be reported in this paper together with a discussion of airspace integration and regulatory topics.

Detect and Avoid↗
NASA NTRSDate not supplied

Assistive Detect and Avoid Technology in Urban Air Mobility Environments

The use of Assistive Detect and Avoid (Assistive DAA or ADAA) technology in Urban Air Mobility (UAM) environments poses potential benefits as well as challenges. Assistive DAA refers to the leveraged use of DAA technology, originally developed to replace see-and-avoid capabilities for remotely piloted aircraft, in onboard-piloted aircraft to augment (rather than replace) pilots’ see-and-avoid abilities and thus enhance the safety and efficiency of visual flight operations. ADAA is anticipated to be especially safety-enhancing in airspace where traffic density is high or traditional air traffic services are limited, such as in future UAM environments. ADAA may also enable higher-tempo UAM operations than with only see-and-avoid capabilities, while still maintaining acceptable levels of safety. UAM concepts under development by the FAA, NASA, and industry focus on operations 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 Langley Research Center, in collaboration with FAA researchers at the William J. Hughes Technical Center in Atlantic City, NJ, have conducted a series of medium-fidelity, human-in-the-loop research simulations of potential future UAM operations and concepts in both Class C and Class B airspace environments. These simulations have included use of a Langley-developed ADAA research tool called DANTi, which enables configurable ADAA displays to be presented to pilots of simulated eVTOL aircraft participating in higher-density and higher-tempo UAM operations. Experience and observations made during testing of the NASA-developed DANTi ADAA capability in the UAM NFLITE simulation environment will be reported in this paper together with a discussion of airspace integration and regulatory topics.

Detect and Avoid↗