Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Copilot”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

44 records · Page 3

ATD Occupant Responses from Three Full-Scale General Aviation Crash Tests

During the summer of 2015, three Cessna 172 General Aviation (GA) aircraft were crash tested at the Landing and Impact Research (LandIR) Facility at NASA Langley Research Center (LaRC). Three different crash scenarios were represented. The first test simulated a flare-to-stall emergency or hard landing onto a rigid surface such as a road or runway. The second test simulated a controlled flight into terrain with a nose down pitch of the aircraft, and the third test simulated a controlled flight into terrain with an attempt to unsuccessfully recover the aircraft immediately prior to impact, resulting in a tail strike condition. An on-board data acquisition system (DAS) captured 64 channels of airframe acceleration, along with accelerations and loads in two onboard Hybrid II 50th percentile Anthropomorphic Test Devices (ATDs) representing the pilot and copilot. Each of the three tests contained different airframe loading conditions and different types of restraints for both the pilot and co-pilot ATDs. The results show large differences in occupant response and restraint performance with varying likelihoods of occupant injury.

Littell, Justin D.↗

Engineering Software for Flight

This talk describes our efforts to improve the software engineering processes of the Copilot runtime verification framework so that the code generated can be used in UAS flights.

software engineering↗

Ground-Based Automated Scheduling for the Mars 2020 Rover

The Mars 2020 Rover Mission will be using an automated ground-based scheduling system called Copilot to schedule the rover’s activities at landing. Using automated scheduling technology will allow for plans to be generated more quickly. Because automated scheduling tools have not been widely used for prior rover missions, developing users’ trust in the system is crucial. An explainable scheduling tool called Crosscheck has been developed to visualize the creation of a schedule, and to explain why activities failed to schedule given their constraints. This will allow science planners to change activity constraints to allow failed activities to successfully schedule, achieving their science goals.

Towey, S.↗

Capturing and Analyzing Requirements with FRET

FRET is an open source tool, developed at NASA Ames, for writing, understanding, formalizing, and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. FRET helps users write FRETish requirements both by providing grammar information and examples during editing, but also through English and diagrammatic explanations to clarify subtle semantic issues. For each requirement, FRET automatically produces formalizations and supports interactive simulation of produced formalizations to ensure that they capture user intentions. Through its analysis portal, FRET connects to analysis tools by exporting verification code. Currently FRET connects to (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs. FRET also supports the consistency/realizability analysis of requirements for identifying conflicting requirements. In this tutorial, we introduce FRET and learn to speak and analyze FRETish through several examples.

FRET↗

FRET Tutorial

In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.

FRET↗

Using FRET to Create, Analyze and Monitor Requirements for a Lift Plus Cruise Case Study

In this technical report we provide information on the use of the NASA Formal RequirementsElicitation Tool (FRET) to create requirements for a Lift Plus Cruise (LPC) aircraft case study. Furthermore, we provide details on using FRET to translate these requirements into an appropriate format for the Copilot tool, enabling their usage to perform runtime verification on a synthesized LPC system.

Formal Requirements Elicitation Tool↗

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↗

Monitoring ROS2: From Requirements to Autonomous Robots

Context/Goals - Capture mission requirements in high-level language. - Monitor requirements for robots. At a Glance - Transform requirements into runtime monitors for ROS2: - Requirements elicitation.* - Transform requirements into Temporal Logic formulas.* - Transform Temporal Logic formulas into runtime monitors.* - Generate hard real-time code for monitors.* - Generate ROS2 application directly from requirements.+ *Steps done in prior work. +Steps extended from prior work.

Runtime verification↗