Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “runtime”

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 NTRS2013

A Scala DSL for RETE-Based Runtime Verification

Runtime verification (RV) consists in part of checking execution traces against formalized specifications. Several systems have emerged, most of which support specification notations based on state machines, regular expressions, temporal logic, or grammars. The field of Artificial Intelligence (AI) has for an even longer period of time studied rule-based production systems, which at a closer look appear to be relevant for RV, although seemingly focused on slightly different application domains, such as for example business processes and expert systems. The core algorithm in many of these systems is the Rete algorithm. We have implemented a Rete-based runtime verification system, named LogFire (originally intended for offline log analysis but also applicable to online analysis), as an internal DSL in the Scala programming language, using Scala's support for defining DSLs. This combination appears attractive from a practical point of view. Our contribution is in part conceptual in arguing that such rule-based frameworks originating from AI may be suited for RV.

matching problem↗
NASA NTRS2015

Environment Modeling Using Runtime Values for JPF-Android

Software applications are developed to be executed in a specific environment. This environment includes external native libraries to add functionality to the application and drivers to fire the application execution. For testing and verification, the environment of an application is simplified abstracted using models or stubs. Empty stubs, returning default values, are simple to generate automatically, but they do not perform well when the application expects specific return values. Symbolic execution is used to find input parameters for drivers and return values for library stubs, but it struggles to detect the values of complex objects. In this work-in-progress paper, we explore an approach to generate drivers and stubs based on values collected during runtime instead of using default values. Entry-points and methods that need to be modeled are instrumented to log their parameters and return values. The instrumented applications are then executed using a driver and instrumented libraries. The values collected during runtime are used to generate driver and stub values on- the-fly that improve coverage during verification by enabling the execution of code that previously crashed or was missed. We are implementing this approach to improve the environment model of JPF-Android, our model checking and analysis tool for Android applications.

Verification↗
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 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 NTRS2020

First-Order Runtime Verification using BDDs

Runtime Verification (RV) expedites the analyses of execution traces for detecting system errors and for statistical and quality analysis. Having started modestly, with checking temporal properties that are based on propositional (yes/no) values, the current practice of RV often involves properties that are parametrized by the data observed in the input trace. The specifications are based on various formalisms, such as automata, temporal logics, rule systems, and stream processing. Checking execution traces that are data intensive against a specification that imposes strong dependencies between the data, poses a nontrivial challenges; in particular if runtime verification has to be performed online, while many events that carry data appear within small time proximities. Towards achieving this goal, it was recently suggested to represent relations over the observed data values, based on BDDs, where data elements are enumerated and then converted into bit vectors. This representation provided a very simple and natural extension of an RV algorithm from propositional to first-order LTL, but more importantly, was shown to contribute to the memory compactness and to the speed, as was demonstrated using a corresponding implementation. We extend here the capabilities of BDD-based RV with the ability to express timing constraints, where the monitored events include (integer) clock values. We show how to efficiently operate on BDDs that represent both relations on (enumerations of) values and time dependencies, as required by the addition of the time constraints. We demonstrate our algorithm with an efficient implementation and provide experimental results.

Peled, Doron↗
NASA NTRS2020

BDDs for Representing Data in Runtime Verification

A BDD (Boolean Decision Diagram) is a data structure for the compact representation of a Boolean function. It is equipped with efficient algorithms for minimization and for applying Boolean operators. The use of BDDs for representing Boolean functions, combined with symbolic algorithms, facilitated a leap in the capability of model checking for the verification of systems with a huge number of states. Recently BDDs were considered as an efficient representation of data for Runtime Verification (RV). We review here the basic theory of BDDs and summarize their use in model checking and specifically in runtime verification.

Peled, Doron↗
NASA NTRS2024

Runtime Thread-Block Optimization for Custom Multistream CUDA Kernels for the Glenn Research Center Communication Analysis Suite

In preparation of the return of humans to the Moon with the coming Artemis missions, NASA scientists must evaluate proposed landing site locations for terrain and communications viability. The Glenn Research Center Communication Analysis Suite (GCAS) combines sophisticated communication network models with accurate lunar terrain to access sites across the Moon’s south pole. Given the importance of proper site selection to crew safety and mission success, many locations need to be analyzed resulting in a large computational load needing to be performed. To meet the growing project demands, development has begun to improve the runtime efficiency of GCAS with GPU parallelization by way of multi-stream CUDA kernels. One of the most prominent factors in kernel optimization is the proper selection of thread-block dimensions in order to maximize the concurrent operation on the device. Typically, thread-block dimensions are optimized by hand requiring many stages of benchmarking and iteration. Additionally, given the main conditions to optimization are the physical GPU architecture and problem size, these optimal dimensions are non-portable and fragile in their scope. As such, a novel optimization routine was developed to generate the optimal thread-block dimensions during runtime with considerations to hardware specifications and problem size resolving the issues of portability and enabling the function of more dynamic routines.

Aden Bergstresser↗
NASA NTRS2023

Runtime Assurance of Aeronautical Products: Preliminary Recommendations

Runtime assurance (RTA) affords an operational layer of protection against safety hazards to aeronautical products that may include less trusted or untrusted functions. However, any RTA scheme must itself be trusted before it can be deployed into use: i.e., it must be fit for its intended purpose, and it must not itself introduce safety hazards. This report contains preliminary recommendations on the application and integration of RTA into aeronautical products intended for use in civil aviation. The main purpose of these recommendations is to inform regulatory guidance and consensus standards that may be used to meet the safety intent of the applicable regulations.

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

Runtime Monitoring with R2U2 for Aircraft Systems with Neural Networks

R2U2 (Realizable, Responsive, Unobtrusive Unit) is a hardware-supported tool and framework for real-time system monitoring and software health management of cyber-physical systems. During system operation, R2U2 continuously monitors properties about safety, performance, and security of the vehicle and its vital components and can perform diagnostic reasoning. Efficient observers for past-time and future-time Metric Temporal Logic, fast reasoners for Bayesian Networks, and model-based prognostics algorithms are key components of R2U2 and designed for minimal computational footprint. R2U2 has been implemented in software supporting ROS, NASA's cFS/cFE, and Simulink and as an FPGA configuration. The synergistic combination of monitors and observers in R2U2 makes it possible to design powerful models for system runtime monitoring, diagnostics, software health management, prognostics, and security monitoring. In this presentation, I will give a detailed overview of the R2U2 architecture and its features and will discuss the application of R2U2 for safety-monitoring of a neural-network based autonomous centerline tracking system (ACT) for autonomous aircraft.

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

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗
NASA NTRS2024

Runtime Verification of Hard Realtime Systems With Copilot: A Tutorial

This presentation is a tutorial on RV using Copilot, 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.

runtime monitoring↗
DOE OSTI2025

IRIS-MEMFLOW: Data Flow-Enabled Portable Memory Orchestration in IRIS Runtime for Diverse Heterogeneity

Task-based programming models and execution paradigms provide a means to decompose a computation by expressing it as a graph in which each node represents a specific computation operating on memory objects and the edges define the dependencies in the execution flow. In this execution model, independent nodes in the graph can be executed concurrently in different computing devices, making it suitable for heterogeneous systems in which computing devices with different architectures coexist. However, careful memory orchestration across heterogeneous devices is needed because copies of the same memory object may reside in multiple devices during execution. Manually ensuring such an orchestration is quite challenging. Not only must an application developer guard against race conditions, but they must also optimize data movement between the host and devices because unnecessary data movement significantly impacts performance. To mitigate these challenges, we enhance the IRIS heterogeneous runtime and introduce IRIS-MEMFLOW–a data flow–enabled portable memory abstraction for seamlessly orchestrating memory in diverse heterogeneous computing environments. By using data-flow analysis, IRIS-MEMFLOW guards against race conditions while multiple heterogeneous devices access memory objects. IRIS-MEMFLOW also optimizes data movement between the host and devices without manual intervention. As a result, IRIS provides improved programming productivity, performance, and portability for multidevice heterogeneous executions in high-performance computing and cloud systems that run diverse architectures from different vendors. The efficacy of IRIS-MEMFLOW is evaluated through experiments that show its capability in terms of programming productivity, multidevice heterogeneity, portability, and low overhead versus the state of the art.

Monil, M. A. H. [ORNL] (ORCID:0000000334194037)↗
DOE OSTI2024

DICER: Data Intensive Computing Environment and Runtime for Evaluating Unprecedented Scale of Geospatial-Temporal Human Mobility Data

With the significant increase in sources and volume of human mobility data through commercial data vendors as well as microsimulation of cities, the scale of geospatial-temporal data to analyze and assess for mobility characterization has grown to the level of Big Data. There are mobility related commercial organizations deploying scalable computing, but often the system architecture, workflow, and intermediate processing components are not fully disclosed in relevant scope. Current research literature has a notable lack of studies demonstrating architectures and workflows for human mobility analytics that are implemented on a TeraByte scale of geospatial-temporal data. In this context, this paper presents a hyperscale-level system solution named DICER (Data Intensive Computing Environment and Runtime) for processing and analytics of geospatial-temporal data at big data scale. Although the cluster computing architecture of DICER with Apache Spark job running on Kubernetes cluster is not new, there are innovations in the workflow, hierarchical processing logic, and a wide range of intermediate preprocessing and mobility metrics calculation. We have performed case studies to validate the effectiveness of DICER system solution by performing detailed analytics and assessment of human mobility microsimulation output at three different scopes and scale, including a usecase with 16.97 TeraByte and 259.2 Billion rows of data. In addition, we have presented another case study of utilizing DICER to perform the same mobility processing and comparative analytics on large-scale commercially available geospatial-temporal data. All these case studies validate the efficiency and usefulness of DICER in computing population mobility characteristics from geospatial-temporal trajectory data at an unprecedented scale (not only just data volume, but also combination of: number of user entities, temporal frequency, spatial resolution, data duration).

De, Debraj↗