Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “embedded systems”

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 127 records · Page 7

Online Planning Algorithm

AVA v2 software selects goals for execution from a set of goals that oversubscribe shared resources. The term goal refers to a science or engineering request to execute a possibly complex command sequence, such as image targets or ground-station downlinks. Developed as an extension to the Virtual Machine Language (VML) execution system, the software enables onboard and remote goal triggering through the use of an embedded, dynamic goal set that can oversubscribe resources. From the set of conflicting goals, a subset must be chosen that maximizes a given quality metric, which in this case is strict priority selection. A goal can never be pre-empted by a lower priority goal, and high-level goals can be added, removed, or updated at any time, and the "best" goals will be selected for execution. The software addresses the issue of re-planning that must be performed in a short time frame by the embedded system where computational resources are constrained. In particular, the algorithm addresses problems with well-defined goal requests without temporal flexibility that oversubscribes available resources. By using a fast, incremental algorithm, goal selection can be postponed in a "just-in-time" fashion allowing requests to be changed or added at the last minute. Thereby enabling shorter response times and greater autonomy for the system under control.

Rabideau, Gregg R.↗

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↗

Interpreter composition issues in the formal verification of a processor-memory module

This report describes interpreter composition techniques suitable for the formal specification and verification of a processor-memory module using the HOL theorem proving system. The processor-memory module is a multichip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. Modeling and verification methods were developed that permit provably secure composition at the transaction-level of specification, significantly reducing the complexity of the hierarchical verification of the system.

Fura, David A.↗

NASA Tech Briefs, September 2012

Topics covered include: Beat-to-Beat Blood Pressure Monitor; Measurement Techniques for Clock Jitter; Lightweight, Miniature Inertial Measurement System; Optical Density Analysis of X-Rays Utilizing Calibration Tooling to Estimate Thickness of Parts; Fuel Cell/Electrochemical Cell Voltage Monitor; Anomaly Detection Techniques with Real Test Data from a Spinning Turbine Engine-Like Rotor; Measuring Air Leaks into the Vacuum Space of Large Liquid Hydrogen Tanks; Antenna Calibration and Measurement Equipment; Glass Solder Approach for Robust, Low-Loss, Fiber-to-Waveguide Coupling; Lightweight Metal Matrix Composite Segmented for Manufacturing High-Precision Mirrors; Plasma Treatment to Remove Carbon from Indium UV Filters; Telerobotics Workstation (TRWS) for Deep Space Habitats; Single-Pole Double-Throw MMIC Switches for a Microwave Radiometer; On Shaft Data Acquisition System (OSDAS); ASIC Readout Circuit Architecture for Large Geiger Photodiode Arrays; Flexible Architecture for FPGAs in Embedded Systems; Polyurea-Based Aerogel Monoliths and Composites; Resin-Impregnated Carbon Ablator: A New Ablative Material for Hyperbolic Entry Speeds; Self-Cleaning Particulate Prefilter Media; Modular, Rapid Propellant Loading System/Cryogenic Testbed; Compact, Low-Force, Low-Noise Linear Actuator; Loop Heat Pipe with Thermal Control Valve as a Variable Thermal Link; Process for Measuring Over-Center Distances; Hands-Free Transcranial Color Doppler Probe; Improving Balance Function Using Low Levels of Electrical Stimulation of the Balance Organs; Developing Physiologic Models for Emergency Medical Procedures Under Microgravity; PMA-Linked Fluorescence for Rapid Detection of Viable Bacterial Endospores; Portable Intravenous Fluid Production Device for Ground Use; Adaptation of a Filter Assembly to Assess Microbial Bioburden of Pressurant Within a Propulsion System; Multiplexed Force and Deflection Sensing Shell Membranes for Robotic Manipulators; Whispering Gallery Mode Optomechanical Resonator; Vision-Aided Autonomous Landing and Ingress of Micro Aerial Vehicles; Self-Sealing Wet Chemistry Cell for Field Analysis; General MACOS Interface for Modeling and Analysis for Controlled Optical Systems; Mars Technology Rover with Arm-Mounted Percussive Coring Tool, Microimager, and Sample-Handling Encapsulation Containerization Subsystem; Fault-Tolerant, Real-Time, Multi-Core Computer System; Water Detection Based on Object Reflections; SATPLOT for Analysis of SECCHI Heliospheric Imager Data; Plug-in Plan Tool v3.0.3.1; Frequency Correction for MIRO Chirp Transformation Spectroscopy Spectrum; Nonlinear Estimation Approach to Real-Time Georegistration from Aerial Images; Optimal Force Control of Vibro-Impact Systems for Autonomous Drilling Applications; Low-Cost Telemetry System for Small/Micro Satellites; Operator Interface and Control Software for the Reconfigurable Surface System Tri-ATHLETE; and Algorithms for Determining Physical Responses of Structures Under Load.

Source record↗

Runtime Verification with Ogma

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enable monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: NASA's Ogma, a tool to transform high-level specifications into monitoring code, and Copilot, a runtime verification framework for real-time embedded systems. The toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware.

Ogma↗

Runtime Verification with Ogma

Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enable monitoring these systems in runtime, to detect property violations early and limit their potential consequences. However, the introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. In this talk we discuss two systems: NASA's Ogma, a tool to transform high-level specifications into monitoring code, and Copilot, a runtime verification framework for real-time embedded systems. The toolchain can be used to translate structured natural language requirements into C code with static memory requirements, which can be compiled to run on embedded hardware.

Ogma↗

Dynamic characterization, monitoring and control of rotating flexible beam-mass structures via piezo-embedded techniques

A variational principle and a finite element discretization technique were used to derive the dynamic equations for a high speed rotating flexible beam-mass system embedded with piezo-electric materials. The dynamic equation thus obtained allows the development of finite element models which accommodate both the original structural element and the piezoelectric element. The solutions of finite element models provide system dynamics needed to design a sensing system. The characterization of gyroscopic effect and damping capacity of smart rotating devices are addressed. Several simulation examples are presented to validate the analytical solution.

Lai, Steven H.-Y.↗

Distributed and parallel Ada and the Ada 9X recommendations

Recently, the DoD has sponsored work towards a new version of Ada, intended to support the construction of distributed systems. The revised version, often called Ada 9X, will become the new standard sometimes in the 1990s. It is intended that Ada 9X should provide language features giving limited support for distributed system construction. The requirements for such features are given. Many of the most advanced computer applications involve embedded systems that are comprised of parallel processors or networks of distributed computers. If Ada is to become the widely adopted language envisioned by many, it is essential that suitable compilers and tools be available to facilitate the creation of distributed and parallel Ada programs for these applications. The major languages issues impacting distributed and parallel programming are reviewed, and some principles upon which distributed/parallel language systems should be built are suggested. Based upon these, alternative language concepts for distributed/parallel programming are analyzed.

Volz, Richard A.↗

Introduction and Highlights of the Workshop

Four generations of CAD/CAM systems can be identified, corresponding to changes in both modeling functionality and software architecture. The systems evolved from 2D and wireframes to solid modeling, to parametric/variational modelers to the current simulation-embedded systems. Recent developments have enabled design engineers to perform many of the complex analysis tasks, typically performed by analysis experts. Some of the characteristics of the current and emerging CAD/CAM/CAE systems are described in subsequent presentations. The focus of the workshop is on the potential of CAD/CAM/CAE systems for use in simulating the entire mission and life-cycle of future aerospace systems, and the needed development to realize this potential. First, the major features of the emerging computing, communication and networking environment are outlined; second, the characteristics and design drivers of future aerospace systems are identified; third, the concept of intelligent synthesis environment being planned by NASA, the UVA ACT Center and JPL is presented; and fourth, the objectives and format of the workshop are outlined.

Noor, Ahmed K.↗

Abstract for 1999 Rational Software User Conference

We develop spacecraft fault-protection software at NASA/JPL. Challenges exemplified by our task: 1) high-quality systems - need for extensive validation & verification; 2) multi-disciplinary context - involves experts from diverse areas; 3) embedded systems - must adapt to external practices, notations, etc.; and 4) development pressures - NASA's mandate of "better, faster, cheaper".

Dunphy, Julia↗

Space Networking Implementation for Lunar Operations

The High-Rate Delay Tolerant Networking (HDTN) project at NASA has developed a performance optimized and open-source Delay Tolerant Networking (DTN) implementation. The primary goal is to create a scalable networking solution to increase the scientific data return rate of space missions. To reach this goal, HDTN must span multiple edge cases in space networking by including tools and configurations to accommodate a wide range of space systems. Typically, HDTN evaluations are conducted on a laboratory emulation test bed, made up of hardware accelerated x86 based systems capable of data rates over 10 Gbps. HDTN must have an effective implementation process on a wide range of systems to increase the sustainability of the design. One important implementation option is with low-level embedded systems which could be used on small robotic missions. This paper details the implementation process, benchmark testing, and performance results of HDTN in multiple configurations on Raspberry Pi 4 devices. By implementing HDTN on a Raspberry Pi 4, a process for building HDTN onto ARM processors was developed and utilized to conduct benchmark tests in multiple network configurations, achieving a data rate performance exceeding 600 Mbps. Based on these results, HDTN proved to run on small ARM based systems with slight modifications to the build procedure. These results were then extended to evaluating an implementation of the HDTN software parsed across several Raspberry Pi 4 nodes. To test this capability, HDTN was configured in a simplified cut-through setup and distributed among multiple Raspberry Pi 4 processors. This distributed architecture was benchmark tested in a similar fashion to the testing of a singular HDTN implementation. The results from the benchmark testing are used to examine how these implementation options and capabilities can expand the use cases for DTN, and particularly with small robotic missions.

Space Networking↗

The formal verification of generic interpreters

The task assignment 3 of the design and validation of digital flight control systems suitable for fly-by-wire applications is studied. Task 3 is associated with formal verification of embedded systems. In particular, results are presented that provide a methodological approach to microprocessor verification. A hierarchical decomposition strategy for specifying microprocessors is also presented. A theory of generic interpreters is presented that can be used to model microprocessor behavior. The generic interpreter theory abstracts away the details of instruction functionality, leaving a general model of what an interpreter does.

Windley, P.↗

Towards the formal verification of the requirements and design of a processor interface unit

The formal verification of the design and partial requirements for a Processor Interface Unit (PIU) using the Higher Order Logic (HOL) theorem-proving system is described. The processor interface unit is a single-chip subsystem within a fault-tolerant embedded system under development within the Boeing Defense and Space Group. It provides the opportunity to investigate the specification and verification of a real-world subsystem within a commercially-developed fault-tolerant computer. An overview of the PIU verification effort is given. The actual HOL listing from the verification effort are documented in a companion NASA contractor report entitled 'Towards the Formal Verification of the Requirements and Design of a Processor Interface Unit - HOL Listings' including the general-purpose HOL theories and definitions that support the PIU verification as well as tactics used in the proofs.

Fura, David A.↗

Engineering Privacy at the Edge: A Practical Guide to Differential Privacy in System Architectures

The rapid expansion of distributed and edge computing platforms—spanning autonomous vehicles, IoT sensors, and healthcare monitors—has heightened concerns about data privacy. Differential Privacy (DP) offers a rigorous mathematical framework to protect sensitive information while retaining analytical utility. This tutorial introduces the foundations of DP for both numerical and categorical datasets and extends the discussion to correlation-aware techniques tailored for structured and high-dimensional data. Hands-on demonstrations will begin with the PETINA (Privacy prEservaTIoN Algorithms) package for numerical data and continue with MIC-DP (Maximum Information Correlated Differential Privacy) for tabular data. Designed for researchers and practitioners in secure systems, embedded architectures, and AI accelerators, the tutorial emphasizes practical and scalable methods for integrating DP into real-world system designs.

Kotevska, Olivera [ORNL] (ORCID:0000000316772243)↗

Neutrino beam bunch structure reconstruction with precision timing in the ICARUS liquid argon time projection chamber

The ICARUS detector has been operating smoothly since 2021 as the far detector in the Short Baseline Neutrino (SBN) program at Fermilab, collecting neutrino interactions from both the Booster Neutrino Beam (BNB) and off-axis from the Neutrinos at the Main Injector (NuMI) beam. Analysis of neutrino interactions in ICARUS requires mitigation of substantial cosmogenic backgrounds. This is achieved by using an external Cosmic Ray Tagger (CRT) and a Photomultiplier Tube (PMT) system embedded in the liquid argon. The intrinsic neutrino beam bunch structure, inherited time structure from the Radio Frequency (RF) system used to accelerate the protons, can be resolved at the ICARUS detector using precise timing information. Located at shallow depth, ICARUS is exposed to a high flux of cosmic rays that can be mistaken for neutrino interactions. To mitigate this background, the CRT and a 3-meter-thick concrete overburden were installed. To better model backgrounds, ICARUS makes use of an overlay technique where simulated neutrino events are superimposed on detector beam-off data. PMTs installed within a Time Projection Chamber detect argon scintillation light emitted by high energy charged particles passing through the chamber and provide the event timing of neutrino interactions. The nanosecond-level beam bunch structure is reconstructed with the PMT system and can be used to further understand backgrounds and enhance neutrino physics capabilities. In this thesis, I will discuss background mitigation techniques using precision timing and present a novel technique to select neutrino events from our unbiased data stream using the beam bunch structure.

Heggestuen, Anna [Colorado State U.] (ORCID:000000↗

Real-Time System Verification by Kappa-Induction

We report the first formal verification of a reintegration protocol for a safety-critical, fault-tolerant, real-time distributed embedded system. A reintegration protocol increases system survivability by allowing a node that has suffered a fault to regain state consistent with the operational nodes. The protocol is verified in the Symbolic Analysis Laboratory (SAL), where bounded model checking and decision procedures are used to verify infinite-state systems by k-induction. The protocol and its environment are modeled as synchronizing timeout automata. Because k-induction is exponential with respect to k, we optimize the formal model to reduce the size of k. Also, the reintegrator's event-triggered behavior is conservatively modeled as time-triggered behavior to further reduce the size of k and to make it invariant to the number of nodes modeled. A corollary is that a clique avoidance property is satisfied.

Pike, Lee S.↗

Efficient and Robust Dynamic Simulation of Power Systems With Holomorphic Embedding

Dynamic simulation is vitally important in power system analysis, but traditional approaches based on numerical integration over small time steps are time-consuming. Also, the Newton-Raphson method suffers from difficulty in convergence when solving nonlinear algebraic equations. In this paper, we propose a novel dynamic simulation approach based on holomorphic embedding. By obtaining a high-order approximation of system dynamics, it achieves a much larger time step and thus enhances the computational efficiency significantly. In addition, the new approach avoids non-convergence issues in solving algebraic equations, which improves robustness. The approach includes flexible modeling of synchronous generators and controllers, and we propose a method for modeling generator coordinate transformations. The approach is tested on the IEEE 39-bus, 10-generator system and a Polish 2383-bus, 327-generator system. The results demonstrate promising computational efficiency and satisfactory numerical robustness for the analysis of large-scale power systems.

42 ENGINEERING↗

Statecharts Via Process Algebra

Statecharts is a visual language for specifying the behavior of reactive systems. The Language extends finite-state machines with concepts of hierarchy, concurrency, and priority. Despite its popularity as a design notation for embedded system, precisely defining its semantics has proved extremely challenging. In this paper, a simple process algebra, called Statecharts Process Language (SPL), is presented, which is expressive enough for encoding Statecharts in a structure-preserving and semantic preserving manner. It is establish that the behavioral relation bisimulation, when applied to SPL, preserves Statecharts semantics

Luttgen, Gerald↗