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

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↗

Runtime Assurance Protection for Advanced Turbofan Engine Control

This paper describes technical progress made in the application of run time assurance (RTA) methods to turbofan engines with advanced propulsion control algorithms that are employed to improve engine performance. It is assumed that the advanced algorithms cannot be fully certified using current verification and validation approaches and therefore need to be continually monitored by an RTA system that ensures safe operation. However, current turbofan engine control systems utilize engine protection logic for safe combustion dynamics and stable airflow through the engine. It was determined that the engine protection logic should continue to be used to provide system safety and should be considered as a part of the overall RTA system. The additional function that an RTA system provides is to perform diagnostics on anomalous conditions to determine if these conditions are being caused by errors in the advanced controller. If this is the case, the RTA system switches operation to a trusted reversionary controller. Initial studies were performed to demonstrate this benefit. The other focus was to improve the performance of the engine protection logic, which was deemed too conservative and reduced engine performance during transient operations. It was determined that the conservative response was due to poor tuning of one of the controller channels within the protection logic. An automatic tuning algorithm was implemented to optimize the protection logic control gains based on minimizing tracking error. Improved tracking responses were observed with no change to the existing protection logic control architecture.

runtime monitoring↗

Runtime Verification

Explore the source record for details and available documents.

Runtime Verification↗

The PARTY parallel runtime system

In the present automated system for the organization of the data and computational operations entailed by parallel problems, in ways that optimize multiprocessor performance, general heuristics for partitioning program data and control are implemented by capturing and manipulating representations of a computation at run time. These heuristics are directed toward the dynamic identification and allocation of concurrent work in computations with irregular computational patterns. An optimized static-workload partitioning is computed for such repetitive-computation pattern problems as the iterative ones employed in scientific computation.

Saltz, J. H.↗

Integrity and security in an Ada runtime environment

A review is provided of the Formal Methods group discussions. It was stated that integrity is not a pure mathematical dual of security. The input data is part of the integrity domain. The group provided a roadmap for research. One item of the roadmap and the final position statement are closely related to the space shuttle and space station. The group's position is to use a safe subset of Ada. Examples of safe sets include the Army Secure Operating System and the Penelope Ada verification tool. It is recommended that a conservative attitude is required when writing Ada code for life and property critical systems.

Bown, Rodney L.↗

Runtime support and compilation methods for user-specified data distributions

This paper describes two new ideas by which an HPF compiler can deal with irregular computations effectively. The first mechanism invokes a user specified mapping procedure via a set of compiler directives. The directives allow use of program arrays to describe graph connectivity, spatial location of array elements, and computational load. The second mechanism is a simple conservative method that in many cases enables a compiler to recognize that it is possible to reuse previously computed information from inspectors (e.g. communication schedules, loop iteration partitions, information that associates off-processor data copies with on-processor buffer locations). We present performance results for these mechanisms from a Fortran 90D compiler implementation.

Ponnusamy, Ravi↗

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↗

Reducing False Positives in Runtime Analysis of Deadlocks

This paper presents an improvement of a standard algorithm for detecting dead-lock potentials in multi-threaded programs, in that it reduces the number of false positives. The standard algorithm works as follows. The multi-threaded program under observation is executed, while lock and unlock events are observed. A graph of locks is built, with edges between locks symbolizing locking orders. Any cycle in the graph signifies a potential for a deadlock. The typical standard example is the group of dining philosophers sharing forks. The algorithm is interesting because it can catch deadlock potentials even though no deadlocks occur in the examined trace, and at the same time it scales very well in contrast t o more formal approaches to deadlock detection. The algorithm, however, can yield false positives (as well as false negatives). The extension of the algorithm described in this paper reduces the amount of false positives for three particular cases: when a gate lock protects a cycle, when a single thread introduces a cycle, and when the code segments in different threads that cause the cycle can actually not execute in parallel. The paper formalizes a theory for dynamic deadlock detection and compares it to model checking and static analysis techniques. It furthermore describes an implementation for analyzing Java programs and its application to two case studies: a planetary rover and a space craft altitude control system.

Bensalem, Saddek↗

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↗

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↗

New Runtime Record Set for Free-Piston Stirling Machine

This article describes the recent progress GRC has made in the arena of long-life heat engines for power conversion. NASA has been interested in Stirling-cycle machines for power conversion since the 1970s. At that time, it was recognized that such a device could be designed to achieve long-life continuous operation with high reliability, by leveraging the free-piston configuration in favor of a kinematic engine. The free-piston variant eliminates the wear mechanisms associated with rolling-element bearings, piston rings, and connecting rods, typically found in kinematic Stirling engine designs. By restricting the moving components to linear motion only, there is no need to convert linear piston movement to rotating motion. With this, the moving components can be suspended within their cylinders by non-contacting bearings and seals can be effected with close clearances, also non-contacting. The use of a linear alternator attached directly to the piston enables direct conversion of heat, to mechanical, then to electrical energy, all in one hermetically sealed vessel, The electrical output only requires simple feedthroughs, and the complexity of sealed a rotating crankshaft is eliminated. In the free-piston variant, the displacer-to-piston phase is not implemented by a connection to a common rotating shaft. Instead, the pressure wave itself is used to drive the displacer. The displacer is designed to have a higher natural frequency of motion than the piston, which achieves a leading phase angle required for power production. The free-piston Stirling behaves like a spring-mass-damper system, with a forcing function created by the alternate heater and cooling of the working gas, and damping provided by the current flowing through the linear alternator. Two types of non-contacting bearings are available to designers: flexure and gas bearings. Flexure bearings consist of a spiral-cut disc of metal that has high radial stiffness but a deliberately engineering stiffness in the axial direction, to permit piston and displacer resonant motion. Gas bearings utilize a pressure source and precisely machined flow channels to provide a radial stiffness around the moving component. The pressure source can be supplied by the engine's pressure wave itself.

Oriti, Salvatore M.↗

Julia Programming Language Benchmark Using a Flight Simulation

Julia’s goal to provide scripting language ease-of-coding with compiled language speed is explored. The runtime speed of the relatively new Julia programming language is assessed against other commonly used languages including Python, Java, and C++. An industry-standard missile and rocket simulation, coded in multiple languages, was used as a test bench for runtime speed. All language versions of the simulation, including Julia, were coded to a highly-developed object-oriented simulation architecture tailored specifically for time-domain flight simulation. A “speed-of-coding” second-dimension is plotted against runtime for each language to portray a space that characterizes Julia’s scripting language efficiencies in the context of the other languages. With caveats, Julia runtime speed was found to be in the class of compiled or semi-compiled languages. However, some factors that affect runtime speed at the cost of ease-of-coding are shown. Julia’s built-in functionality for multi-core processing is briefly examined as a means for obtaining even faster runtime speed. The major contribution of this research to the extensive language benchmarking body-of-work is comparing Julia to other mainstream languages using a complex flight simulation as opposed to benchmarking with single algorithms.

Sells, Ray↗

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↗