Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “runtime monitoring”

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.

At least 91 records · Page 5
All sourcesNASA NTRSDOE OSTI
NASA NTRS2015

A Flexible and Non-instrusive Approach for Computing Complex Structural Coverage Metrics

Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (MC/DC). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code. Furthermore, instrumented code cannot be used in conjunction with other analyses that reason about the structure and semantics of the code under test. In this work, we introduce a non-intrusive preprocessing approach for computing structural coverage information. It uses a static partial evaluation of the decisions in the source code and a source-to-bytecode mapping to generate the information necessary to efficiently track structural coverage metrics during execution. Our technique is flexible; the results of the preprocessing can be used by a variety of coverage-driven software analysis tasks, including automated analyses that are not possible for instrumented code. Experimental results in the context of symbolic execution show the efficiency and flexibility of our nonintrusive approach for computing code coverage information

DO-178C↗
NASA NTRS2018

Runtime Verification: From Propositional to First-Order Temporal Logic

Runtime Verification is a branch of formal methods concerned with analysis of execution traces for the purpose of determining the state or general quality of the executing system. The field covers numerous approaches, one of which is specification-based runtime verification, where execution traces are checked against formal specifications. The paper presents syntax, semantics, and monitoring algorithms for respectively propositional and first-order temporal logics. In propositional logics the observed events in the execution trace are represented using atomic propositions, while first-order logic allows universal and existential quantification over data occurring as arguments in events. Monitoring of the first-order case is drastically more challenging than the propositional case, and we present a solution for this problem based on BDDs. We furthermore discuss monitorability of temporal properties by dividing them into different classes representing different degrees of monitorability.

Peled, Doron↗
NASA NTRS2020

Actor-based Runtime Verification with MESA

This work presents a runtime verification approach implemented in the tool MESA (MEssage-based System Analysis) which allows for using concurrent monitors to check for properties specified in data parameterized temporal logic and state machines. The tool is implemented as an internal Scala DSL. We employ the actor programming model to implement MESA where monitors are captured by concurrent actors that communicate via messaging. The paper presents a case study in which MESA is used to effectively monitor a large number of flights from live US airspace data streams. We also perform an empirical study by conducting experiments using monitoring systems with different num- bers of concurrent monitors and different layers of indexing on the data contained in events. The paper describes the experiments, evaluates the results, and discusses challenges faced during the study. The evaluation shows the value of combining concurrency with indexing to handle data rich events.

Mehlitz, Peter↗
NASA NTRS2018

BDDs on the Run

Runtime verification (RV) of first-order temporal logic must handle a potentially large amount of data, accumulated during the monitoring of an execution. The DEJAVU RV system represents data elements and relations using BDDs. This achieves a compact representation, which allows monitoring long executions. However, the potentially unbounded, and frequently very large amounts of data value scan,ultimately, limit the executions that can be monitored. We present an automatic method for “forgetting” data values when they no longer affect the RV verdict on an observed execution.We describe the algorithm and illustrate its operation through an example.

Peled, Doron↗
NASA NTRS2018

The DejaVu Runtime Verification Benchmark

In this paper we present a benchmark for evaluating runtime verification tools. It was originally created in order to compare the DEJAVU runtime verification tool1 with another similar tool. DEJAVU’s logic is first-order past time temporal logic. In order to monitor such properties efficiently, Binary Decision Diagrams (BDDs) [1] are used for representing the data observed in a trace. The details on the logic and its algorithm are described in e.g. [2, 3, 4]. The benchmark consists of six properties, formulated in English, and formalized in DEJAVU’s logic. For each property is provided (normally) three traces, of sizes varying from 10,000 events to one million events. Traces are represented in CSV format.

Ulus, Dogan↗
NASA NTRS2017

R2U2: Tool Overview

R2U2 (Realizable, Responsive, Unobtrusive Unit) is an extensible framework for runtime System HealthManagement (SHM) of cyber-physical systems. R2U2 can be run in hardware (e.g., FPGAs), or software; can monitorhardware, software, or a combination of the two; and can analyze a range of different types of system requirementsduring runtime. An R2U2 requirement is specified utilizing a hierarchical combination of building blocks: temporal formula runtime observers (in LTL or MTL), Bayesian networks, sensor filters, and Boolean testers. Importantly, the framework is extensible; it is designed to enable definitions of new building blocks in combination with the core structure. Originally deployed on Unmanned Aerial Systems (UAS), R2U2 is designed to run on a wide range of embedded platforms, from autonomous systems like rovers, satellites, and robots, to human-assistive ground systems and cockpits. R2U2 is named after the requirements it satisfies; while the exact requirements vary by platform and mission, the ability to formally reason about realizability, responsiveness, and unobtrusiveness is necessary for flight certifiability, safety-critical system assurance, and achievement of technology readiness levels for target systems. Realizability ensures that R2U2 is suficiently expressive to encapsulate meaningful runtime requirements while maintaining adaptability to run on different platforms, transition between different mission stages, and update quickly between missions. Responsiveness entails continuously monitoring the system under test, real-time reasoning, reporting intermediate status, and as-early-as-possible requirements evaluations. Unobtrusiveness ensures compliance with the crucial properties of the target architecture: functionality, certifiability, timing, tolerances, cost, or other constraints.

Rozier, Kristin Y.↗
NASA NTRS2009

Analog Input Data Acquisition Software

DAQ Master Software allows users to easily set up a system to monitor up to five analog input channels and save the data after acquisition. This program was written in LabVIEW 8.0, and requires the LabVIEW runtime engine 8.0 to run the executable.

Arens, Ellen↗
NASA NTRS2017

Unobtrusive Software and System Health Management with R2U2 on a Parallel MIMD Coprocessor

Dynamic monitoring of software and system health of a complex cyber-physical system requires observers that continuously monitor variables of the embedded software in order to detect anomalies and reason about root causes. There exists a variety of techniques for code instrumentation, but instrumentation might change runtime behavior and could require costly software re-certification. In this paper, we present R2U2E, a novel realization of our real-time, Realizable, Responsive, and Unobtrusive Unit (R2U2). The R2U2E observers are executed in parallel on a dedicated 16-core EPIPHANY co-processor, thereby avoiding additional computational overhead to the system under observation. A DMA-based shared memory access architecture allows R2U2E to operate without any code instrumentation or program interference.

Schumann, Johann↗
NASA NTRS2017

MESA: Message-Based System Analysis Using Runtime Verification

In this paper, we present a novel approach and framework for run-time verication of large, safety critical messaging systems. This work was motivated by verifying the System Wide Information Management (SWIM) project of the Federal Aviation Administration (FAA). SWIM provides live air traffic, site and weather data streams for the whole National Airspace System (NAS), which can easily amount to several hundred messages per second. Such safety critical systems cannot be instrumented, therefore, verification and monitoring has to happen using a nonintrusive approach, by connecting to a variety of network interfaces. Due to a large number of potential properties to check, the verification framework needs to support efficient formulation of properties with a suitable Domain Specific Language (DSL). Our approach is to utilize a distributed system that is geared towards connectivity and scalability and interface it at the message queue level to a powerful verification engine. We implemented our approach in the tool called MESA: Message-Based System Analysis, which leverages the open source projects RACE (Runtime for Airspace Concept Evaluation) and TraceContract. RACE is a platform for instantiating and running highly concurrent and distributed systems and enables connectivity to SWIM and scalability. TraceContract is a runtime verication tool that allows for checking traces against properties specified in a powerful DSL. We applied our approach to verify a SWIM service against several requirements.We found errors such as duplicate and out-of-order messages.

Message-based System↗
NASA NTRS2005

BEAM Technology Flight Demonstration

As technologies advance, their growing complexity makes them harder to maintain. Detection methods for isolating and identifying impending problems are needed to balance this complexity. Through comparison of signal pairs from onboard sensors, the Beacon-based Exception Analysis For Multimissions (BEAM) algorithm can identify and help classify deviations in system operation from a data-trained statistical model. The goal of this task is to mature BEAM and validate its performance on a flying test bed. A series of F-18 flight demonstrations with BEAM monitoring engine parameters in real time was used to demonstrate in-the-field readiness. Captured F-18 and simulated F-18 engine data were used in model creation and training. The algorithm was then ported to the embedded system with a data buffering, file writing, and data-time-stamp monitoring shell to reduce the impact of embedded system faults on BEAM'S ability to correctly identify engine faults. Embedded system testing identified hardware related restrictions and contributed to iterative improvements in the code's runtime performance. The system was flown with forced engine flameouts and other pilot induced faults to simulate operation out of the norm. Successful detection of these faults, confirmed through post-flight data analysis, helped BEAM achieve TRL6.

Wang, David↗
NASA NTRS2004

ScyFlow: An Environment for the Visual Specification and Execution of Scientific Workflows

With the advent of grid technologies, scientists and engineers are building more and more complex applications to utilize distributed grid resources. The core grid services provide a path for accessing and utilizing these resources in a secure and seamless fashion. However what the scientists need is an environment that will allow them to specify their application runs at a high organizational level, and then support efficient execution across any given set or sets of resources. We have been designing and implementing ScyFlow, a dual-interface architecture (both GUT and APT) that addresses this problem. The scientist/user specifies the application tasks along with the necessary control and data flow, and monitors and manages the execution of the resulting workflow across the distributed resources. In this paper, we utilize two scenarios to provide the details of the two modules of the project, the visual editor and the runtime workflow engine.

McCann, Karen M.↗
NASA NTRS2024

Components Refurbishment and Chemical Analysis Facility, Hot Spot 1 Solid Waste Management Unit #041 Year 4 Annual Performance Monitoring Report Kennedy Space Center, Florida

This Year 4 Annual Performance Monitoring Report (PMR) presents the operations, maintenance, and monitoring activities for the Hydraulic Containment System (HCS) Interim Measure (IM) at the Components Refurbishment and Chemical Analysis (CRCA) facility located at John F. Kennedy Space Center (KSC), Florida. The primary objective of the HCS is to attain hydraulic control of the dissolved-phase chlorinated volatile organic compound (CVOC) plume, with the secondary objective to reduce concentrations of CVOCs in the high-concentration plume to support transition to monitored natural attenuation (MNA). CRCA has been designated Solid Waste Management Unit 041 under the KSC Resource Conservation and Recovery Act Corrective Action Program. The timeframe for activities documented in this Year 4 PMR extends from November 2022 through September 2023. Baseline sampling activities were completed in June 2019, and full-scale startup of the HCS IM was completed in July-August 2019. The operational runtime of the HCS for the Year 4 reporting period was approximately 94%, with the majority of downtime attributed to associated groundwater sampling events, maintenance, and Hurricane Nicole. Almost five million gallons of groundwater were treated during Year 4 of HCS operations, and concentrations of the site’s contaminants of concern (trans-1,2-dichloroethene and vinyl chloride) have been reduced by over 99%. This PMR describes the activities that were performed during Year 4 to operate and monitor the HCS IM, which includes three extraction wells, seven injection wells, and conveyance piping to a modular structure containing the control panel and an air stripper. Influent and effluent sampling results from the air stripper show that the system is operating as designed and is reducing concentrations of contaminants of concern to below detection limits. In addition to HCS operation, this PMR also discusses performance monitoring that has been implemented to assess progress of the HCS IM and overall plume conditions through scheduled groundwater (quarterly and semi-annual) and sub-slab soil gas (quarterly) sampling and analysis. Two ambient air samples were also collected on a quarterly basis in the vicinity of the modular structure and the paved driveway east of the Solvent Reclamation Area during routine operation and maintenance (O&M) activities to ensure safe breathing zone air quality for on-site personnel. All sub-slab soil gas and ambient air sampling conducted during the Year 4 operational period showed results below applicable regulatory air screening limits. Predictions made during the Year 2 groundwater model updates were in close correlation to post Year 4 plume conditions. A supplemental DPT study conducted in 2022 and 2023. This study indicated that low-concentration plume conditions, where concentrations exceed State of Florida Groundwater Cleanup Target Levels, expanded westward to Kennedy Parkway North and northward to the vicinity of the railroad tracks. Based on these results, recommendations were made to install 14 wells to monitor the downgradient and boundary conditions of the expanded LCP. The contents of this Year 4 PMR were presented during the November 2023 KSC Remediation Team meeting, where Team consensus was reached on several items including continued O&M of the HCS, and continued monitoring of groundwater, ambient air, and sub-slab soil gas. Sampling for per- and polyfluoroalkyl substances at CRCA is ongoing and will be submitted under separate cover.

K. Alex Murphy↗
NASA NTRS2023

Components Refurbishment and Chemical Analysis Facility, Hot Spot 1 SWMU #041 Year 3 Annual Performance Monitoring Report Kennedy Space Center, Florida

This Year 3 Annual Performance Monitoring Report (PMR) presents the operations, maintenance, and monitoring activities for the Hydraulic Containment System (HCS) Interim Measure (IM) at the Components Refurbishment and Chemical Analysis (CRCA) facility located at John F. Kennedy Space Center (KSC), Florida. The primary objective of the HCS is to attain hydraulic control of the dissolved-phase chlorinated volatile organic compound (CVOC) plume, with the secondary objective to reduce concentrations of CVOCs in the high-concentration plume to support transition to monitored natural attenuation (MNA). CRCA has been designated Solid Waste Management Unit 041 under the KSC Resource Conservation and Recovery Act Corrective Action Program. The timeframe for activities documented in this Year 3 PMR extends from September 2021 through October 2022. Baseline sampling activities were completed in June 2019, and full-scale startup of the HCS IM was completed in July-August 2019. The operational runtime of the HCS for the Year 3 reporting period was approximately 91%, with the majority of downtime attributed to system maintenance and repair. This is generally consistent with Year 1 and Year 2 runtimes of 85% and 92%, respectively. To help reduce downtime, an anti-scaling amendment, Redux 390, has been used to reduce scaling and help maintain system design parameters. Over nine million gallons of groundwater were treated during Year 3 of HCS operations, and concentrations of the site’s contaminants of concern (trans-1,2-dichloroethene and vinyl chloride) have been reduced by over 97%. This PMR describes the activities that were performed during Year 3 to operate and monitor the HCS IM, which includes three extraction wells, seven injection wells, and conveyance piping to a modular structure containing the control panel and an air stripper. Influent and effluent sampling results from the air stripper show that the system is operating as designed and is reducing concentrations of contaminants of concern to below detection limits. In addition to HCS operation, this PMR also discusses performance monitoring that has been implemented to assess progress of the HCS IM and overall plume conditions through scheduled groundwater (quarterly and semi-annual) and sub-slab soil gas (quarterly) sampling and analysis. Two ambient air samples were also collected on a quarterly basis in the vicinity of the modular structure and the paved driveway east of the Solvent Reclamation Area during routine operation and maintenance (O&M) activities to ensure safe breathing zone air quality for on-site personnel. All sub-slab soil gas and ambient air sampling conducted during the Year 3 operational period showed results below applicable regulatory air screening limits. Predictions made during the Year 2 groundwater model updates were in close correlation to post Year 3 plume conditions. Therefore, it can be assumed that the projected path remains valid for transition to MNA in one to two years of continuous HCS operation. The contents of this Year 3 PMR were presented during the February 2023 KSC Remediation Team meeting, where Team consensus was reached on several items including continued O&M of the HCS, and continued monitoring of groundwater, ambient air, and sub-slab soil gas. Replacement of MW0019 and VMP04 was also recommended, as well as additional direct-push technology sampling to further delineate the downgradient plume and confirm overall site-wide low-concentration plume boundaries. Sampling for per- and polyfluoroalkyl substances at CRCA is ongoing and will be submitted under separate cover.

K. Alex Murphy↗
NASA NTRS2008

Orchestrator Telemetry Processing Pipeline

Orchestrator is a software application infrastructure for telemetry monitoring, logging, processing, and distribution. The architecture has been applied to support operations of a variety of planetary rovers. Built in Java with the Eclipse Rich Client Platform, Orchestrator can run on most commonly used operating systems. The pipeline supports configurable parallel processing that can significantly reduce the time needed to process a large volume of data products. Processors in the pipeline implement a simple Java interface and declare their required input from upstream processors. Orchestrator is programmatically constructed by specifying a list of Java processor classes that are initiated at runtime to form the pipeline. Input dependencies are checked at runtime. Fault tolerance can be configured to attempt continuation of processing in the event of an error or failed input dependency if possible, or to abort further processing when an error is detected. This innovation also provides support for Java Message Service broadcasts of telemetry objects to clients and provides a file system and relational database logging of telemetry. Orchestrator supports remote monitoring and control of the pipeline using browser-based JMX controls and provides several integration paths for pre-compiled legacy data processors. At the time of this reporting, the Orchestrator architecture has been used by four NASA customers to build telemetry pipelines to support field operations. Example applications include high-volume stereo image capture and processing, simultaneous data monitoring and logging from multiple vehicles. Example telemetry processors used in field test operations support include vehicle position, attitude, articulation, GPS location, power, and stereo images.

Powell, Mark↗
NASA NTRS2024

Former Central Heat Plant SWMU 045 Year 2 Air Sparge System Performance Monitoring Report

This Air Sparge (AS) Performance Monitoring (PM) Report (PMR) presents Year 2 operation, maintenance, and monitoring (OM&M) activities, PM results, and monitoring well installations supporting the AS Interim Measure (IM) at the Former Central Heat Plant (CHP) at Kennedy Space Center (KSC), Florida. CHP has been designated Solid Waste Management Unit 045 under the KSC Resource Conservation and Recovery Act Corrective Action Program. An AS IM was installed at CHP between 2019 and 2021, which included the installation of an AS system to treat a chlorinated solvent groundwater plume. Contaminants of concern (COCs) identified at CHP for the AS IM include tetrachloroethene (PCE), trichloroethene (TCE), cis-1,2-dichloroethene (cDCE), and vinyl chloride (VC). The completed AS system includes a network of 267 AS wells, which treat approximately 1.3 acres of contaminated groundwater. “Hot” compressor technology is used to treat the source zone, while a “cold” compressor is used to treat two hot spot (HS) areas (HS1 and HS2) and the high concentration plume (HCP). The AS system began operation in June-July 2021 and this document includes Year 2 of operation. The overall runtimes for the AS system for the Year 2 reporting period (October 2022 to September 2023) were approximately 69 percent for the cold trailer and 71 percent for the hot trailer. Air samples and vapor screening results collected during the reporting period showed concentrations less than applicable human health and air emissions permit criteria. Groundwater performance monitoring results show that AS treatment continues to be effective in reducing COC concentrations at CHP. At the shallow interval, COC concentrations were all non-detect, less than, or met their respective State of Florida Groundwater Cleanup Target Levels (GCTLs) at the end of Year 2 in September 2023. In the deep interval, 10 of the 15 PM wells detected COCs greater than their respective GCTLs, with two of these wells also exceeding the Natural Attenuation Default Concentration for VC. Based on Year 2 OM&M and PM results, continued operation of the AS system is required to meet the IM objective. It is therefore recommended to continue with AS IM operations at CHP with the following plan for Year 3.

Kevin Alex Murphy↗
NASA NTRS2023

Launch Complex 34, SWMU CCO542022 DNAPL Source Zone Operations, Maintenance, and Monitoring, Site-Wide Long-Term Monitoring, and Hot Spot 6 Air Sparge System Annual Performance Monitoring Report Cape Canaveral Space Force Station, Florida

This Annual Performance Monitoring Report (PMR) for the Dense Non-Aqueous Phase Liquid (DNAPL) Source Zone (DSZ), Site-Wide Long-Term Monitoring (LTM), and Hot Spot (HS) 6 Air Sparge (AS) System presents the results of Year 13 operation of the hydraulic containment (HC) Interim Measure (IM), the results of performance monitoring direct-push technology (DPT) sampling and monitoring well sampling conducted in the DSZ, results of the biennial site-wide LTM event, and the results of operations and performance sampling of the HS 6 AS IM at Launch Complex 34 (LC34), located at Cape Canaveral Space Force Station (CCSFS), Florida. This site has been designated Solid Waste Management Unit (SWMU) CC054 under the Kennedy Space Center (KSC) Resource Conservation and Recovery Act (RCRA) Corrective Action Program. For the site-wide biennial LTM event, a total of 55 monitoring wells were sampled for volatile organic compounds (VOCs) in February 2023 and one well was sampled for polychlorinated biphenyls (PCBs) in December 2022. One well planned for VOC sampling was found to be destroyed and could not be sampled (CW0002). The LTM wells are screened in two lithologic zones: Layer 1 (0 to 25 feet below land surface [bls]) and Layer 2 (25 to 30 ft bls), and are located in the outlying areas of LC34 to monitor groundwater conditions within the Low-Concentration Plume (LCP), defined as concentrations exceeding Groundwater Cleanup Target Levels (GCTLs), and the High-Concentration Plume (HCP), defined as concentrations exceeding Natural Attenuation Default Concentrations (NADCs). Results from the biennial sampling event indicated overall plume stability and delineation for the plume, which extends over 300 acres. The operational period for Year 13 of the HCS was from April 1, 2022 to March 31, 2023. Operational runtime for the system was 90 percent during Year 13, with downtime events attributed to planned maintenance, system repairs, and power outages. As of March 31, 2023, a total of 313,673,241 cumulative gallons of groundwater containing 88,337 pounds of VOCs have been removed by the HCS. Influent concentrations of trichloroethene (TCE) have decreased since startup from approximately 280,000 μg/L (January 2010) to 12,000 μg/L (March 2023). During the reporting period, all effluent concentrations from the HCS (aqueous and vapor) were below regulatory reporting limits, indicating the system continues to operate as intended. Performance monitoring was conducted in December 2022 within the DSZ to evaluate TCE contamination. Groundwater samples were collected via DPT at nine locations, consistent with previous events between 2017 and 2021. Full vertical profile sampling was completed at each DPT from 8 to 98 feet bls, at 5-foot intervals. The DPT performance monitoring results are summarized in this PMR. The results revealed TCE remains at concentrations greater than 11,000 μg/L in the DSZ (1-percent solubility, indicative of DNAPL) at eight of the nine DPT locations and at depths ranging from 8 to 98 feet bls. In addition to DPT sampling, groundwater samples were collected from deep monitoring wells in the DSZ area (Layers 7 and 8) in December 2022 to verify vertical delineation. Layer 7/8 monitoring well results were non-detect in December 2022, with exception of three wells (IW0162, IW043D2, and IW044D2), where TCE, cis-1,2-dichloroethene (cDCE), and/or vinyl chloride (VC) were detected above GCTLs. These wells are screened 105 to 115 feet bls, which is below the existing recovery well capture zone. TCE was first detected in IW0162 in December 2021 and has since been sampled at least monthly to monitor TCE concentrations. The maximum TCE concentration during this operational period was 15,000 μg/L at IW0162 in March 2023. Because of the increased TCE concentrations in this well, a new recovery well (RW21D), screened 86 to 106 feet bls, was installed in January 2023 and incorporated into existing HCS operations. The HS 6 AS IM was initiated in 2018 with 160 AS wells, and expanded in 2019 with an additional 140 AS wells. Quarterly performance monitoring was reduced to semi-annual in 2020. The HS 6 AS system remained operational during the reporting period covered under this report. The results of the HS 6 system operation and semi-annual performance monitoring are summarized in this report. Semi-annual monitoring results collected in April and October 2022 show concentrations of contaminants of concern (cDCE, trans-1,2-dichloroethene, and vinyl chloride) are generally decreasing and not impacting the surface water drainage canal, indicating the HS 6 IM is meeting objectives. A Phase Two Expansion of the HS 6 AS IM was recently completed. As of the date of this report, the expansion became operational in August 2023 and the first quarter of monitoring was conducted in November 2023. Details of the construction, start-up, and performance monitoring will be included in a future Annual PMR. Overall, the tasks associated with Year 13 operation of the HC IM, operation of the HS 6 AS IM, and biennial site-wide sampling were performed in accordance with recommendations included in the previous 2021 LC34 (Year 12) annual report. Evaluation of results from the HC IM and HS 6 IM show that these systems are operating as designed and meeting performance objectives. Results from the site-wide biennial LTM program also show that the overall network of monitoring wells is adequate to continue monitoring plume-wide conditions.

Complex 34↗
NASA NTRS2023

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↗