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 73 records · Page 4
All sourcesNASA NTRSDOE OSTI
NASA NTRS2014

Data Automata in Scala

The field of runtime verification has during the last decade seen a multitude of systems for monitoring event sequences (traces) emitted by a running system. The objective is to ensure correctness of a system by checking its execution traces against formal specifications representing requirements. A special challenge is data parameterized events, where monitors have to keep track of the combination of control states as well as data constraints, relating events and the data they carry across time points. This poses a challenge wrt. efficiency of monitors, as well as expressiveness of logics. Data automata is a form of automata where states are parameterized with data, supporting monitoring of data parameterized events. We describe the full details of a very simple API in the Scala programming language, an internal DSL (Domain-Specific Language), implementing data automata. The small implementation suggests a design pattern. Data automata allow transition conditions to refer to other states than the source state, and allow target states of transitions to be inlined, offering a temporal logic flavored notation. An embedding of a logic in a high-level language like Scala in addition allows monitors to be programmed using all of Scala's language constructs, offering the full flexibility of a programming language. The framework is demonstrated on an XML processing scenario previously addressed in related work.

runtime verification↗
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 NTRS2017

Runtime Verification Logics A Language Design Perspective

Runtime Verification is a light-weight approach to systems verification, where actual executions of a system are processed and analyzed using rigorous techniques. In this paper we shall narrow the term’s definition to represent the commonly studied variant consisting of verifying that a single system execution conforms to a specification written in a formal specification language. Runtime verification (in this sense) can be used for writing test oracles during testing when the system is too complex for full formal verification, or it can be used during deployment of the system as part of a fault protection strategy, where corrective actions may be taken in case the specification is violated. Specification languages for runtime verification appear to differ from for example temporal logics applied in model checking, in part due to the focus on monitoring of events that carry data, and specifically due to the desire to relate data values existing at different time points, resulting in new challenges in both the complexity of the monitoring approach and the expressiveness of languages. Over the recent years, numerous runtime verification specification languages have emerged, each with its different features and levels of expressiveness and usability. This paper presents an overview and a discussion of this design space.

Reger, Giles↗
NASA NTRS2008

Runtime Verification of C Programs

We present in this paper a framework, RMOR, for monitoring the execution of C programs against state machines, expressed in a textual (nongraphical) format in files separate from the program. The state machine language has been inspired by a graphical state machine language RCAT recently developed at the Jet Propulsion Laboratory, as an alternative to using Linear Temporal Logic (LTL) for requirements capture. Transitions between states are labeled with abstract event names and Boolean expressions over such. The abstract events are connected to code fragments using an aspect-oriented pointcut language similar to ASPECTJ's or ASPECTC's pointcut language. The system is implemented in the C analysis and transformation package CIL, and is programmed in OCAML, the implementation language of CIL. The work is closely related to the notion of stateful aspects within aspect-oriented programming, where pointcut languages are extended with temporal assertions over the execution trace.

RMOR↗
NASA NTRS2003

The Mobile Agents Integrated Field Test: Mars Desert Research Station April 2003

The Mobile Agents model-based, distributed architecture, which integrates diverse components in a system for lunar and planetary surface operations, was extensively tested in a two-week field "technology retreat" at the Mars Society s Desert Research Station (MDRS) during April 2003. More than twenty scientists and engineers from three NASA centers and two universities refined and tested the system through a series of incremental scenarios. Agent software, implemented in runtime Brahms, processed GPS, health data, and voice commands-monitoring, controlling and logging science data throughout simulated EVAs with two geologists. Predefined EVA plans, modified on the fly by voice command, enabled the Mobile Agents system to provide navigation and timing advice. Communications were maintained over five wireless nodes distributed over hills and into canyons for 5 km; data, including photographs and status was transmitted automatically to the desktop at mission control in Houston. This paper describes the system configurations, communication protocols, scenarios, and test results.

Clancey, William J.↗
NASA NTRS2001

Java PathExplorer: A Runtime Verification Tool

We describe recent work on designing an environment called Java PathExplorer for monitoring the execution of Java programs. This environment facilitates the testing of execution traces against high level specifications, including temporal logic formulae. In addition, it contains algorithms for detecting classical error patterns in concurrent programs, such as deadlocks and data races. An initial prototype of the tool has been applied to the executive module of the planetary Rover K9, developed at NASA Ames. In this paper we describe the background and motivation for the development of this tool, including comments on how it relates to formal methods tools as well as to traditional testing, and we then present the tool itself.

Havelund, Klaus↗
NASA NTRS2003

Rule-Based Runtime Verification

We present a rule-based framework for defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time logics, interval logics, forms of quantified temporal logics, and so on. Our logic, EAGLE, is implemented as a Java library and involves novel techniques for rule definition, manipulation and execution. Monitoring is done on a state-by-state basis, without storing the execution trace.

Barringer, Howard↗
NASA NTRS2014

Monitoring with Data Automata

We present a form of automaton, referred to as data automata, suited for monitoring sequences of data-carrying events, for example emitted by an executing software system. This form of automata allows states to be parameterized with data, forming named records, which are stored in an efficiently indexed data structure, a form of database. This very explicit approach differs from other automaton-based monitoring approaches. Data automata are also characterized by allowing transition conditions to refer to other parameterized states, and by allowing transitions sequences. The presented automaton concept is inspired by rule-based systems, especially the Rete algorithm, which is one of the well-established algorithms for executing rule-based systems. We present an optimized external DSL for data automata, as well as a comparable unoptimized internal DSL (API) in the Scala programming language, in order to compare the two solutions. An evaluation compares these two solutions to several other monitoring systems.

log analysis↗
NASA NTRS2002

An Overview of the Runtime Verification Tool Java PathExplorer

We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into efficient automata, which check the event stream. JPAX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.

Havelund, Klaus↗
NASA NTRS2021

Concurrent Runtime Verification of Data Rich Events

This paper presents the open source runtime verification tool MESA (MEssage-based System Analysis), implemented in Scala, which supports concurrent monitors using the Actor model. Furthermore, the tool supports indexing (slicing) on the data values occurring in data-carrying events, for each individual monitor. The tool is generic in the sense that any monitoring system can be used for creating monitors. In this paper, we use the internal Scala DSL Daut for programming such in data parameterized state machines and temporal logic. To illustrate MESA/Daut, we present a case study that monitors flights from live U.S. airspace data streams, verifying that they conform to planned routes. With base in the case study, we then perform an extensive empirical study of the potential benefits from monitoring slices of a single property in concurrently executing actors. Due to the overhead of scheduling “small” actors (one for each slice or a small number of slices), it is not obvious that concurrent execution of such is beneficial. However, as a main result, we demonstrate that concurrent monitoring of slices to handle data-carrying events can provide considerable speed gains.

finite state machines↗
NASA NTRS2011

Runtime Verification with State Estimation

We introduce the concept of Runtime Verification with State Estimation and show how this concept can be applied to estimate theprobability that a temporal property is satisfied by a run of a program when monitoring overhead is reduced by sampling. In such situations, there may be gaps in the observed program executions, thus making accurate estimation challenging. To deal with the effects of sampling on runtime verification, we view event sequences as observation sequences of a Hidden Markov Model (HMM), use an HMM model of the monitored program to "fill in" sampling-induced gaps in observation sequences, and extend the classic forward algorithm for HMM state estimation (which determines the probability of a state sequence, given an observation sequence) to compute the probability that the property is satisfied by an execution of the program. To validate our approach, we present a case study based on the mission software for a Mars rover. The results of our case study demonstrate high prediction accuracy for the probabilities computed by our algorithm. They also show that our technique is much more accurate than simply evaluating the temporal property on the given observation sequences, ignoring the gaps.

sampling↗
NASA NTRSDate not supplied

Satellite-assisted Evaluation of Irrigation Application Efficiency for Lettuce in the Salinas Valley

The Salinas Valley region of California’s Central Coast is a majorU.S. vegetable producer. Lettuce is a leading commodity, grown on about 100,000 acres with annual value near $1.4B (2022 Monterey County Ag Report). Vegetables crops in the area aretypically well watered and fertilized in pursuit of commercial yield and quality standards. Information on irrigation application efficiency, meanwhile, can enhance waterresource sustainability and mitigate impacts of nitrate infiltrationon groundwater quality. The Crop Consumptive Use Fraction (CCUF), previously recommended by the California Department of Water Resources, is a metric that expresses evapotranspiration (ET) of applied water relative to total applied water. More recently under Assembly Bill 1668 addressing water conservation and drought planning, the metric can be used to help quantify application efficiency to support preparation of agricultural water management plans in the state. This study will report CCUF evaluations from several commercial lettuce plantings in the Salinas Valley during the 2022 dry season (late spring-early fall). The evaluations were derived from satellite-based observations of cropET from the OpenETcloud application, and applied water monitored by in-line flowmetersand supplemented by grower reports of irrigation system runtime. The study will also compare observed (satellite-based) ET with modeled ET from the CropManage irrigationand nutrient management decision-support system operated by Cooperative Extension. Additional study in cool-season vegetables is ongoing in 2023.

Satellite-assisted↗
NASA NTRSDate not supplied

MESA: Scalable Runtime Verification Tool Using Actors

This work presents our runtime verification approach implemented by the tool MESA (MEssage-based System Analysis) which allows for using concurrent monitors to check for properties specified in linear temporal logic and finite state machines.We employ the actor programing model to implement MESA where monitors are captured by concurrent actors that communicate via messaging. The paper also presents a case study where MESA is used to monitor flights in National Airspace System of United States using live air traffic data stream. The case study which motivated this work in the first place shows that our approach is effective.We also perform empirical study by conducting experiments using monitoring systems with different numbers of concurrent monitors and different layers of indexing.This paper describes our experiments, evaluates our results,and discusses challenges faced during the study. The evaluation shows our approach is scalable.

runtime verification, concurrency, actor programin↗
NASA NTRS2022

Chile Disasters: Automating Wildfire Risk and Occurrence Mapping in Google Earth Engine to Improve Wildfire Detection and Response Time Efforts

Wildfires in Chile in the last decade were the worst on record, destroying homes and livelihoods, polluting the air, and displacing whole towns. To predict locations where wildfires were likely to start, the Corporación Nacional Forestal (CONAF) created a wildfire risk model within ArcGIS Pro and Google Earth Engine (GEE) that utilized the NOAA Global Forecast System (GFS) and the NASA Shuttle Radar Topography Mission (STRM) 90-meter datasets. The previous CONAF model was very resource-heavy and time-intensive to run. NASA DEVELOP, in partnership with CONAF, automated the previous model and transferred it fully into GEE where all Earth observation datasets could be used without downloading. The new model substantially reduced the runtime. The final model was used to create a near real-time wildfire monitoring application as well as fire severity maps. The end products will be used by CONAF for wildfire prediction and management to prevent more destruction in the future.

Maria De Los Santos↗
NASA NTRSDate not supplied

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 numbers 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.

runtime verification↗
NASA NTRS2024

Launch Complex 39B, SWMU 009, 2023 Performance Monitoring and Air Sparge Expansion Construction Completion Report, Kennedy Space Center, Florida

The 2023 Performance Monitoring and Construction Completion Report (PM-CCR) presents the findings, observations, and results for Air Sparging (AS) operations and expansion activities, as well as sitewide groundwater monitoring for Launch Complex 39B (LC39B), Solid Waste Management Unit (SWMU) 009, at Kennedy Space Center (KSC), Florida. The reporting period for activities covered under this PM-CCR is from January 1, 2023, to December 31, 2023. At LC39B, AS operations began in 2017 in the area west of the launch pad, in the liquid oxygen (LOX) tank area located northwest of the launch pad, and in an area outside of the perimeter fence to protect nearby Outstanding Florida Waters (OFW). The LC39B AS system was installed with 279 AS wells to depths ranging from 23 to 60 feet below land surface (bls), including the sump, correlating to top of screen depths ranging from 20 to 57 feet bls. In December 2022, a total of 22 AS wells were abandoned to support launch pad crane operations, and in November 2023, the system was expanded with five additional AS wells installed to 13 or 17 feet bls near the LOX tank. The remedial objective of the LC39B AS Interim Measure (IM) is to actively decrease concentrations of contaminants of concern (COCs) in groundwater, specifically trichloroethene (TCE), cis-1,2-Dichloroethene (cDCE), and vinyl chloride (VC), to less than their respective Natural Attenuation Default Concentrations (NADCs), so LC39B can transition into a Long-Term Monitoring (LTM) program. This PM-CCR presents the following information for LC39B: • AS system operations and maintenance (O&M) (Year 7 of operation) from January 2023 to December 2023, to include AS trailer relocation in March 2023 and subsequent replacement and re-start in June 2023. • Construction completion details for AS system expansion, which included installation of five new AS wells and one new monitoring well in November 2023. As part of expansion activities, soil samples were also collected for petroleum analysis; no exceedances were identified, and no further investigation for petroleum is warranted. • Performance monitoring results for groundwater sampling events conducted in May/June 2023 (30 wells) and November 2023 (31 wells) in the AS IM area and in the Low Concentration Plume (LCP) areas located north and east of the launch pad for volatile organic compound (VOC) analysis. • Sampling results for one monitoring well, LOX-IW0012S, which is sampled for aluminum on an annual basis (May/June 2023). This well was resampled in November 2023 for both total and dissolved aluminum. Due to a communication error with the laboratory, the May/June 2023 sample was analyzed for total aluminum only. • Groundwater sampling results for per- and polyfluoroalkyl substances (PFAS) collected from seven monitoring wells during the May/June 2023 event to further investigate the Former Sewage Treatment Plant #6 and Percolation Pond area, west of the launch pad. O&M and performance monitoring results show that the AS system at LC39B is operating as designed and meeting performance criteria. Overall runtime was 45 percent (%) during the reporting period (January to December), but the operational runtime was 78% during the timeframe when the system could run (June to December). The most significant downtime contributor was post-launch crane operations following the Artemis launch on November 16, 2022, which lasted until June 2023. During that timeframe, the AS trailer at LC39B was relocated to another KSC remediation site (Wilson Corners) and was subsequently replaced with the AS trailer from the Paint & Oil Locker (POL) remediation site at KSC to resume AS system operations. Performance monitoring results in the AS IM and LCP areas continue to show reduction in COC concentrations over time when compared to baseline levels. In 2023, only one monitoring well (MW0048) detected a COC exceeding its NADC (VC at 740 micrograms per liter [µg/L]), which marks the baseline result for this new well installed during system expansion. Across the rest of the site, VC concentrations have declined or remained stable during the 2023 sampling events. Excluding MW0048, the highest VC result in 2023 was during the May/June sampling event with a concentration of 63 µg/L at MW0032, which is located near MW0048 and the AS expansion area by the LOX tank. TCE was detected in select monitoring wells in the IM area in 2023, but only two locations exceeded the State of Florida Groundwater Cleanup Target Level (GCTL): MW0032 (21 µg/L in May/June 2023 and 9.1 µg/L in November 2023) and MW0036 (5.0 µg/L in November 2023). MW0036 is also located near the LOX tank, on the north side, where the AS system is still operational (Zone Z4). cDCE and trans-1,2-dichloroethene concentrations were less than laboratory method detection limits or their respective GCTLs in all wells sampled in 2023. Near the OFW located northwest of the launch complex, all COC concentrations were less than laboratory method detection limits from monitoring wells (MW0039, MW0040, and LOXTA0002S) sampled in 2023. Aluminum results from LOX-IW0012S, which has been sampled routinely since 2006, detected a total aluminum concentration of 3,900 µg/L during the May/June 2023 sampling event. Results from the November 2023 event detected 5,700 µg/L for total aluminum and 5,500 µg/L for dissolved aluminum. These concentrations slightly decreased from the previous year but remain relatively consistent with historical detections. Aluminum will continue to be sampled on an annual basis at this well as results still exceed the GCTL of 200 µg/L and the Upper Limit of the KSC Background Concentration of 280 µg/L. PFAS results detected nine different PFAS compounds (out of 32 analyzed) from seven wells sampled. Two PFAS compounds, perfluorooctanesulfonic acid (PFOS) and perfluorooctanoic acid (PFOA), currently have FDEP Provisional GCTLs of 70 nanograms per liter (ng/L). All seven samples collected resulted in concentrations less than the FDEP Provisional GCTLs for both PFAS compounds; no exceedances were observed. PFOS and PFOA also have assigned United States Environmental Protection Agency (USEPA) Maximum Contaminant Levels (MCLs) of 4 nanograms per liter (ng/L). None of the PFOS results exceeded the USEPA MCLs. PFOA was detected in two samples above the USEPA MCL at concentrations of 5.8 ng/L (ECS-IW0009I) and 5.5 ng/L (ECS-IW0009S). Three other PFAS compounds, perfluorohexanesulfonic acid (PFHxS), perfluoro-n-nonanoic acid (PFNA), and hexafluoropropylene oxide dimer acid (GenX), currently have USEPA MCLs of 10 ng/L. PFHxS, PFNA, and GenX were not detected at concentrations greater than their respective USEPA MCLs in any of the seven wells. PFAS compounds without FDEP Provisional GCTLs or USEPA MCLs were screened against USEPA RSLs. No other detections exceeded their respective USEPA RSLs. Additional PFAS sampling will be conducted as part of a future PFAS Site Assessment. Based on O&M activities and performance monitoring, the following is recommended for LC39B: • Continue with Year 8 AS system operation within Zone Z4, which includes the AS expansion area. Zone Z3, which has been off since 2018, should remain off as no rebound has been observed. Zones Z1 and Z2, which were turned off at the end of 2022, will remain shut down as monitoring well results have consistently been below GCTLs or have low-level detections with stable or decreasing trends (Meeting Minute 2402-M10, Decision 2402-D30). • Continue with performance monitoring in 2024 with the same monitoring well network as 2023, except with the addition of MW0048 in both semi-annual events. Baseline concentrations for this well were collected during the November 2023 performance monitoring event. Semi-annual sampling should be planned for the May 2024 and November 2024 timeframes (Meeting Minute 2402-M10, Decision 2402-D31). • Continue sampling monitoring well, LOX-IW0012S, for aluminum (total and dissolved) on an annual basis in May 2024. It is also recommended to re-develop this well prior to the next sampling event (Meeting Minute 2402-M10, Decision 2402-D32). The above recommendations for LC39B were presented at the February 2024 KSCRT Meeting, with Team consensus reached on the path forward. The contents of this PM-CCR were also presented at this meeting.

Deborah M Wilson↗
NASA NTRS1998

A Discussion of Issues in Integrity Constraint Monitoring

In the development of large-scale software systems, analysts, designers, and programmers identify properties of data objects in the system. The ability to check those assertions during runtime is desirable as a means of verifying the integrity of the program. Typically, programmers ensure the satisfaction of such properties through the use of some form of manually embedded assertion check. The disadvantage to this approach is that these assertions become entangled within the program code. The goal of the research is to develop an integrity constraint monitoring mechanism whereby a repository of software system properties (called integrity constraints) are automatically inserted into the program by the mechanism to check for incorrect program behaviors. Such a mechanism would overcome many of the deficiencies of manually embedded assertion checks. This paper gives an overview of the preliminary work performed toward this goal. The manual instrumentation of constraint checking on a series of test programs is discussed, This review then is used as the basis for a discussion of issues to be considered in developing an automated integrity constraint monitor.

Fernandez, Francisco G.↗
NASA NTRSDate not supplied

Swarm Mentality: Toward Automatic Swarm State Awareness with Runtime Verification

Cyber-Physical Systems (CPSs) already exhibit impressive performance in all areas of human life, and swarms of CPSs promise to increase their capabilities even further. However, to effectively utilize CPS swarms their complexity of operation has to scale sub-linearly with the number of swarm members. Presenting the swarm to an operator as a single entity almost eliminates the additional per-member overhead entirely. To operate a swarm as one entity, and/or to increase the swarm’s autonomy, the operator and the swarm members need to reason and communicate at the same level of abstraction, i.e. the swarm needs a sense of “self.” Therefore, we require the ability to specify whole swarm properties yet monitor them at the member level. We examine one architecture for achieving this awareness by: 1) Defining a taxonomy for comparing techniques that synthesize this belief-state 2) Propose use of the Runtime Verification formal method to fill this role 3) Present preliminary designs for extending and embedding such a system in the Distributed Spacecraft Autonomy architecture to generate per-member monitors from swarm level specification.

Runtime Verification↗