Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Criticality Safety”

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 451 records · Page 25
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

A Verification Framework for Runtime Assurance of Autonomous UAS

Runtime Assurance (RTA) is a design-time architecture for safety-critical systems where an internal monitor acts upon detecting a violation of a property. The simplex architecture is an instance of RTA, where the action taken is to hand control of the overall system to a trusted controller when an untrusted one violates a safety property. Simplex RTA is emerging as a method for allowing AI/ML and other unverified software to be integrated into safety-critical applications like aircraft. To this end, the American Society for Testing and Materials (ASTM) and NASA have each published guidelines on the use of RTA in such systems. In the simplex RTA framework, a system has an advanced controller (AC) and a reversionary controller (RC). The system is allowed to operate with the AC until a runtime monitor detects that some property has been violated and then the RC takes over. Assuming that the sample rate of the monitor will detect improper functioning with enough time for the RC to correct the impending problem, and that the RC is trusted, the system will operate as intended. This use of the simplex RTA framework can allow for the integration of untrusted, but possibly more performant, controllers in a safe way. This paper presents a formalization of a simplex RTA framework in the Prototype Verification System (PVS) theorem prover using an embedding of differential dynamic logic (DDL) called Plaidypvs. A novel feature of this framework is that it can be instantiated at different levels of abstraction. This feature allows for the formal verification of a system with an untrusted black box component, such as an AI/ML controller. This paper does not address the many difficulties in deploying RTA in an industrial-level system. Instead, the focus is on the formal verification of the simplex RTA framework in the language of hybrid programs. Hybrid programs are programs that include both discrete and continuous dynamics and can be used to model complex cyber-physical systems. Plaidypvs is a tool that enables formalization of hybrid programs in the PVS theorem prover. Plaidypvs enables the verification of the general simplex RTA framework and then, by specializing some components of the hybrid program, verifying instances of the framework while treating the untrusted component as a black box. A selection of Unmanned Aircraft Systems (UAS) operations are shown as instances of the general RTA framework in PVS. This offers the benefit of design time verification of relevant safety properties to the system, and it also gives requirements on the sample rate of sensors that determine the time interval in which the ‘switch’ property of the RTA framework is checked.

PVS↗
NASA NTRS2004

A Tool for Verification and Validation of Neural Network Based Adaptive Controllers for High Assurance Systems

High reliability of mission- and safety-critical software systems has been identified by NASA as a high-priority technology challenge. We present an approach for the performance analysis of a neural network (NN) in an advanced adaptive control system. This problem is important in the context of safety-critical applications that require certification, such as flight software in aircraft. We have developed a tool to measure the performance of the NN during operation by calculating a confidence interval (error bar) around the NN's output. Our tool can be used during pre-deployment verification as well as monitoring the network performance during operation. The tool has been implemented in Simulink and simulation results on a F-15 aircraft are presented.

Gupta, Pramod↗
NASA NTRS2008

NASA Langley's Formal Methods Research in Support of the Next Generation Air Transportation System

This talk will provide a brief introduction to the formal methods developed at NASA Langley and the National Institute for Aerospace (NIA) for air traffic management applications. NASA Langley's formal methods research supports the Interagency Joint Planning and Development Office (JPDO) effort to define and develop the 2025 Next Generation Air Transportation System (NGATS). The JPDO was created by the passage of the Vision 100 Century of Aviation Reauthorization Act in Dec 2003. The NGATS vision calls for a major transformation of the nation s air transportation system that will enable growth to 3 times the traffic of the current system. The transformation will require an unprecedented level of safety-critical automation used in complex procedural operations based on 4-dimensional (4D) trajectories that enable dynamic reconfiguration of airspace scalable to geographic and temporal demand. The goal of our formal methods research is to provide verification methods that can be used to insure the safety of the NGATS system. Our work has focused on the safety assessment of concepts of operation and fundamental algorithms for conflict detection and resolution (CD&R) and self- spacing in the terminal area. Formal analysis of a concept of operations is a novel area of application of formal methods. Here one must establish that a system concept involving aircraft, pilots, and ground resources is safe. The formal analysis of algorithms is a more traditional endeavor. However, the formal analysis of ATM algorithms involves reasoning about the interaction of algorithmic logic and aircraft trajectories defined over an airspace. These trajectories are described using 2D and 3D vectors and are often constrained by trigonometric relations. Thus, in many cases it has been necessary to unload the full power of an advanced theorem prover. The verification challenge is to establish that the safety-critical algorithms produce valid solutions that are guaranteed to maintain separation under all possible scenarios. Current research has assumed perfect knowledge of the location of other aircraft in the vicinity so absolute guarantees are possible, but increasingly we are relaxing the assumptions to allow incomplete, inaccurate, and/or faulty information from communication sources.

Butler, Ricky W.↗
DOE OSTI2022

Effects of Chlorine Capture and a Proposed Density Law on the Reactivity of Plutonium Solution Systems

During fissionable material processing, all normal and credible abnormal conditions must remain safely subcritical. Nuclear Criticality Safety (NCS) uses a number of methods to determine subcriticality, one of which is the use of neutron transport codes such as MCNP6. In order to create models for use with MCNP6, both the geometry and materials in fissionable material processes must be known, or assumptions must be made and quantified for the impact to bias. One of the systems with a significant amount of bias due to material modeling assumptions is in the area of aqueous plutonium processing. These solutions are typically plutonium nitrate solutions or plutonium chloride solutions, which are modeled as fictitious plutonium metal-water mixtures because little is known about the actual density of the solution and there is no current predictive capability approved for use at Los Alamos National Laboratory (LANL) for modeling them. This research is currently underway to fill the gap and develop an algorithm for use with MCNP6 to model the density of plutonium chloride solutions. The method is to be validated with experimental data for density, and also validated with critical experiments using MCNP6. Note that the Chlorine Worth Study (CWS) was performed in December 2021 to help bridge the gap in chlorine data for critical experiments, and is currently awaiting International Criticality Safety Benchmark Evaluation Project (ICSBEP) review. This study was performed by LANL at the National Criticality Experiments Research Center (NCERC) at the Nevada National Security Site (NNSS). Additional information regarding this experiment may currently be found in LA-UR- 22-29180. Additionally, the Chemistry-Actinide Analytical Chemistry (C-AAC) at LANL has performed a number of solution density measurements for PuCl 3 -HC 1 -H 2 O, allowing for such data be used to create a semi-empirical density via the Pitzer method. The published dataset for the measurements is documented in LA-UR-22-25454. This method has already been tested successfully for aqueous plutonium nitrate solutions in SCALE. Current solution density measurements exist of plutonium concentrations of 0-~142g/L, all at 2M HC1, at temperatures 20-40°C. Additional data was taken for HC1-corrected density values, which essentially mimics the data for a pure PuCl x -water solution. The calculations in this report aim to support the current research by demonstrating the difference in system reactivity for the current modeling method when compared to the new proposed modeling with a density law implementation, which is being written as a Python tool to be used with MCNP6.

38 RADIATION CHEMISTRY, RADIOCHEMISTRY, AND NUCLEA↗
NASA NTRS2006

Time Triggered Protocol (TTP) for Integration Modular Avionics (IMA)

This viewgraph presentation is a review of the Time Triggered Protocol, designed to work with NASA's Integrated Safety-Critical Advanced Avionics Communication and Control (ISAACC) system. ISAACC is the product of the Propulsion High-Impact Avionics Technologies (PHIAT) project at NASA Marshall Space Flight Center (MSFC) during FY03 to the end of FY05. The goal is an avionics architecture suitable for control and monitoring of safety critical systems of manned spacecraft. It must be scalable to allow its use in robotic vehicles or launch pad and propulsion test stand monitoring and control systems. The developed IMA should have: a common power supply and rugged chassis for a set of modules, many upgradeable software functions on one module (i.e. processing unit Reduced weight, straightforward update and system integration. It is also important that it have Partitioning and a Memory Management Unit (MMU)

Gwaltney, David A.↗
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 NTRS2015

Software Graphics Processing Unit (sGPU) for Deep Space Applications

A graphics processing capability will be required for deep space missions and must include a range of applications, from safety-critical vehicle health status to telemedicine for crew health. However, preliminary radiation testing of commercial graphics processing cards suggest they cannot operate in the deep space radiation environment. Investigation into an Software Graphics Processing Unit (sGPU)comprised of commercial-equivalent radiation hardened/tolerant single board computers, field programmable gate arrays, and safety-critical display software shows promising results. Preliminary performance of approximately 30 frames per second (FPS) has been achieved. Use of multi-core processors may provide a significant increase in performance.

McCabe, Mary↗
DOE OSTI2025

Benchmark Gap Assessment for the Manufacturing of High-Assay Low-Enriched Uranium Fuels

This document develops basic critical conditions for spheres—moderated and unmoderated, as well as reflected and unreflected—in consideration of nuclear criticality safety of a potential fuel production facility producing high-assay low-enriched uranium (HALEU) fuel of several different types like tristructural-isotropic (TRISO), uranium metal and alloys, oxide and non-metallic forms. In addition to spherical arrangements, TRISO particle manufacturing process–specific equipment is modeled as it would be for the criticality safety analysis. The objective is to develop representative systems that can then be used for comparison with existing benchmarks. SCALE/TSUNAMI is used to assess the similarity index between these systems to assess validation gaps for possible fuel production applications of proposed advanced reactors. Several different fuel types were evaluated, including TRISO, uranium metal, uranium molybdenum, uranium zirconium, uranium dioxide, uranium nitride, uranium hydride, U-ZrH, and uranium chloride. This selection of fuel types covers a breadth of proposed reactor types, as well as intermediate steps in the production and fabrication of the fuel

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2025

Impact of recent ENDF nuclear data update, high initial enrichment and high burnup fuel on critical experiments applicability determination via the integral index c k for burnup credit validation

In 2012, NUREG/CR-7109 reported on the validation of burnup credit calculations involving major and minor actinides and major fission products which was investigated for pressurized and boiling water reactor (PWR and BWR) fuel enrichments up to 5 wt% 235 U and assembly-average burnups up to 60 GWd/MTU. Recently, there has been interest in increasing the maximum enrichment used in PWR fuel as high as 8 wt% 235 U and correspondingly increasing the maximum assembly-average burnups to approximately 75 GWd/MTU. These proposed increases in enrichment and burnup necessitate reinvestigation of the validation basis for k eff calculations for this expanded application space. Additionally, the 2012 study was performed by using the Evaluated Nuclear Data File (ENDF)/B-VII.0 nuclear data with the SCALE 6 covariance library, and the effects of using the newly released ENDF/B-VII.1 and ENDF/B-VIII.0 nuclear data and covariance libraries should be evaluated. In this work, published in NUREG/CR-7309 in 2025, the validation assessment was performed consistently with NUREG/CR-7109: modeling irradiated fuel assemblies in the Generic Burnup Credit (GBC)-32 cask defined in NUREG/CR-6747. The TSUNAMI-3D sequence was used to generate sensitivity data for the application model, and the data were compared with sensitivity data from select benchmark models. The integral parameter c k is the metric of similarity used in this study and is consistent with NUREG/CR-7109, where a c k value in excess of 0.8 indicates sufficient similarity for use in validation. A new set of benchmark experiments with sensitivity data has been assembled for this effort. The number of experiments with available sensitivity data is now 2,104, compared to 474 in NUREG/CR-7109. This increase was facilitated by the efforts of the Nuclear Energy Agency to generate sensitivity data for a majority of the experiments in the International Criticality Safety Benchmark Evaluation Project (ICSBEP) Handbook to supplement the data available in the Oak Ridge National Laboratory (ORNL) Verified, Archived Library of Inputs and Data (VALID). The complete set of benchmarks considered here includes experiments for low-enriched uranium (LEU), intermediate enriched uranium (IEU), and a mixture of uranium and plutonium (MIX) from the ICSBEP Handbook and VALID, as well as ORNL models of the Haut Taux de Combustion (HTC) experiments and other potentially relevant models not included in VALID. The updated similarity study shows that none of the extended burnup and higher enrichment combinations considered show a significant decrease in the number of potentially applicable experiments, meaning sufficient critical experiments exist for the validation of BUC criticality safety calculations, with initial enrichments up to 8 wt% 235 U and burnups up to 80 GWd/MTU. Additionally, both the ENDF/B-VII.1 and ENDF/B-VIII.0 nuclear data libraries can be used for validation since the number of critical experiments applicable for validation increases for most cases with the most recent nuclear data compared to the previous one. As in previous BUC validation studies, the French HTC experiments are the most similar in a majority of the application cases studied, especially from representative discharge burnups ranging from 40 to 80 GWd/MTU. In conclusion, these results match the conclusions presented in NUREG/CR-7109 regarding validation of the primary actinides in BUC analyses.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗
DOE OSTI2025

Control Selection for the Neutralization Tank in the Aqueous Recovery System at the Savannah River Plutonium Processing Facility

The Aqueous Recovery System (ARS) at the Savannah River Plutonium Processing Facility (SRPPF) recovers and purifies plutonium (Pu) using aqueous chemistry techniques. The neutralization tanks in the ARS collect the waste streams, containing various impurities and greatly reduced concentrations of Pu, that are produced during aqueous processing. Criticality safety is primarily achieved in the ARS by using geometrically favorable process vessels. However, due to the geometry of neutralization tanks, each tank is administratively limited to no more than 450 g Pu, thus representing the transition from geometry to mass control. To ensure that this mass limit is not exceeded, an administrative control requires taking two samples of any solution to be sent to a neutralization tank. Normal operations are expected to result in less than 50 g Pu in a neutralization tank filled to its capacity of 250 L. Process upsets may cause an inadvertent transfer of up to 1000 g Pu to a neutralization tank, producing a system that is potentially not subcritical for all possible configurations of the tank. To ensure that a neutralization tank remains safety subcritical, passive engineered controls (e.g.changing tank geometry or adding fixed poisons), active engineered controls (e.g. interlocks), and administrative controls (e.g. soluble poisons and valve isolation) were considered and their viability evaluated. Ultimately, the team chose an administrative, dual-valve isolation strategy. This paper will thoroughly discuss the various control strategy options and why many of the options were not feasible for maintaining criticality safety.

Dressman, Phillip M. [Savannah River Nuclear Solut↗
DOE OSTI2025

Control Selection for the Neutralization Tank in the Aqueous Recovery System at the Savannah River Plutonium Processing Facility

The Aqueous Recovery System (ARS) at the Savannah River Plutonium Processing Facility (SRPPF) recovers and purifies plutonium (Pu) using aqueous chemistry techniques. The neutralization tanks in the ARS collect waste streams with various impurities and greatly reduced concentrations of Pu than are produced during aqueous processing. Criticality safety is primarily achieved in the ARS by using geometrically favorable process vessels. However, due to the geometry of neutralization tanks, each tank is administratively limited to no more than 450 g Pu, thus representing the transition from geometry to mass control. To ensure that this mass limit is not exceeded, an administrative control requires taking two samples of any solution to be sent to a neutralization tank. Normal operations are expected to result in less than 50 g Pu in a neutralization tank filled to its capacity of 250 L. Process upsets may cause an inadvertent transfer of up to 1000 g Pu to a neutralization tank, producing a system that is potentially not subcritical for all possible configurations of the tank. To ensure that a neutralization tank remains safety subcritical, passive engineered controls (e.g. changing tank geometry or adding fixed poisons), active engineered controls (e.g. interlocks), and administrative controls (e.g. soluble poisons and valve isolation) were considered and their viability evaluated. Ultimately, the team chose an administrative, dual-valve isolation strategy. This paper will thoroughly discuss the various control strategy options and why many of the options were not feasible for maintaining criticality safety.

Dressman, Phillip M. [Savannah River Nuclear Solut↗
NASA NTRS2006

Autonomy Software: V&V Challenges and Characteristics

The successful operation of unmanned air vehicles requires software with a high degree of autonomy. Only if high level functions can be carried out without human control and intervention, complex missions in a changing and potentially unknown environment can be carried out successfully. Autonomy software is highly mission and safety critical: failures, caused by flaws in the software cannot only jeopardize the mission, but could also endanger human life (e.g., a crash of an UAV in a densely populated area). Due to its large size, high complexity, and use of specialized algorithms (planner, constraint-solver, etc.), autonomy software poses specific challenges for its verification, validation, and certification. -- - we have carried out a survey among researchers aid scientists at NASA to study these issues. In this paper, we will present major results of this study, discussing the broad spectrum. of notions and characteristics of autonomy software and its challenges for design and development. A main focus of this survey was to evaluate verification and validation (V&V) issues and challenges, compared to the development of "traditional" safety-critical software. We will discuss important issues in V&V of autonomous software and advanced V&V tools which can help to mitigate software risks. Results of this survey will help to identify and understand safety concerns in autonomy software and will lead to improved strategies for mitigation of these risks.

Schumann, Johann↗
DOE OSTI2021

A High-Assay Low-Enriched Uranium Fuel Transportation Concept

The uranium 235U enrichment commonly used in fuel production for U.S. light water nuclear reactors typically does not exceed 5 wt%. In contrast, many of the currently investigated advanced reactor concepts demand fuel with higher enrichments. This includes high-assay low-enriched uranium (HALEU), characterized by a 235U enrichment of 5 to 20 wt%. The necessity of HALEU transportation in the fuel production cycle leads to new challenges caused by various technical and regulatory hurdles. Current U.S. Nuclear Regulatory Commission–approved transportation package designs for UF6 with enrichments above 5 wt% provide relatively small payloads [=116 kg (250 lb)]. Furthermore, in accordance with 10 CFR 71.55, package design activities for fissile material enriched above 5 wt% need to consider water infiltration in the containment as part of the criticality safety evaluations. This study presents a transportation package concept for HALEU advanced nuclear reactor fuel with a significantly higher payload of up to 376 kg (830 lb) of fissile material per package and up to 1881 kg (4149 lb) of HALEU per legal weight truck. The anticipated chemical form of the transported material is UO2 downblended from available highly enriched uranium. The concept utilizes a combination of existing transportation packaging, 18 inner canisters, and a novel basket design that includes a borated aluminum flux trap. Criticality and shielding evaluations; fundamental structural, confinement, and thermal assessments; and studies on package operations are presented. The results of this study build significant confidence in the technical feasibility of a high-capacity HALEU transportation package concept while demonstrating the concept’s potential to meet U.S. regulatory requirements.

Eidelpes, Elmar↗
NASA NTRSDate not supplied

Probability of Obstacle Collision for UAVs in Presence of Wind

For incorporation of unmanned aerial vehicles into the National Airspace, ensuring safety of the airspace including the vehicles, people, and property on the ground is of utmost importance. One of the safety-critical factors for unmanned aviation flights is the risk of deviating from a planned trajectory resulting in a variety of hazards, including potential loss of separation between vehicle and obstacles or unexpected battery energy consumption. Off-nominal conditions introduced by component failures, degraded controllability and environmental disturbances such as wind gusts can lead to unacceptable unexpected deviations from the flight trajectory. It is essential to accurately model such effects on the flight trajectory while computing safety thresholds such as minimum separation from surrounding obstacles, available battery resource to complete the mission or determining delay in the expected time of arrival of flights. In this paper, a tool is presented based on Gaussian Process Regression for wind representation over a pre-defined trajectory for fast, yet approximated, in-time evaluation of possible trajectory deviations caused by wind gusts. The deviation in the planned trajectory caused by wind is further simulated utilizing a 6 degrees-of-freedom (DOF) UAV trajectory simulator comprising of a rotorcraft lumped-mass model with LQRI controller. Both steady-state wind and wind gust effects are investigated. The probability of collision with obstacle is computed and demonstrated on real flight data from experimental flights of an octocopter at NASA Langley Research Center in the presence of simulated obstacles and wind conditions. Effect of varying wind conditions and varying UAV airspeed is further demonstrated on experimental flights in the presence of wind measured by ground based weather service stations. The proposed approach would eventually benefit timely mitigation of current and future safety-critical events in autonomous systems by enabling risk-informed decision making.

Portia Banerjee↗
NASA NTRS2017

Command and Control Software Development Memory Management

This internship was initially meant to cover the implementation of unit test automation for a NASA ground control project. As is often the case with large development projects, the scope and breadth of the internship changed. Instead, the internship focused on finding and correcting memory leaks and errors as reported by a COTS software product meant to track such issues. Memory leaks come in many different flavors and some of them are more benign than others. On the extreme end a program might be dynamically allocating memory and not correctly deallocating it when it is no longer in use. This is called a direct memory leak and in the worst case can use all the available memory and crash the program. If the leaks are small they may simply slow the program down which, in a safety critical system (a system for which a failure or design error can cause a risk to human life), is still unacceptable. The ground control system is managed in smaller sub-teams, referred to as CSCIs. The CSCI that this internship focused on is responsible for monitoring the health and status of the system. This team's software had several methods/modules that were leaking significant amounts of memory. Since most of the code in this system is safety-critical, correcting memory leaks is a necessity.

Programmin↗
NASA NTRS2018

Verification and Validation Challenges for Adaptive Flight Control of Complex Autonomous Systems

Autonomy of aerospace systems requires the ability for flight control systems to be able to adapt to complex uncertain dynamic environment. In spite of the five decades of research in adaptive control, the fact still remains that currently no adaptive control system has ever been deployed on any safety-critical or human-rated production systems such as passenger transport aircraft. The problem lies in the difficulty with the certification of adaptive control systems since existing certification methods cannot readily be used for nonlinear adaptive control systems. Research to address the notion of metrics for adaptive control began to appear in the recent years. These metrics, if accepted, could pave a path towards certification that would potentially lead to the adoption of adaptive control as a future control technology for safety-critical and human-rated production systems. Development of certifiable adaptive control systems represents a major challenge to overcome. Adaptive control systems with learning algorithms will never become part of the future unless it can be proven that they are highly safe and reliable. Rigorous methods for adaptive control software verification and validation must therefore be developed to ensure that adaptive control system software failures will not occur, to verify that the adaptive control system functions as required, to eliminate unintended functionality, and to demonstrate that certification requirements imposed by regulatory bodies such as the Federal Aviation Administration (FAA) can be satisfied. This presentation will discuss some of the technical issues with adaptive flight control and related V&V challenges.

Nguyen, Nhan T.↗
NASA NTRS2008

Certifying Auto-Generated Flight Code

Model-based design and automated code generation are being used increasingly at NASA. Many NASA projects now use MathWorks Simulink and Real-Time Workshop for at least some of their modeling and code development. However, there are substantial obstacles to more widespread adoption of code generators in safety-critical domains. Since code generators are typically not qualified, there is no guarantee that their output is correct, and consequently the generated code still needs to be fully tested and certified. Moreover, the regeneration of code can require complete recertification, which offsets many of the advantages of using a generator. Indeed, manual review of autocode can be more challenging than for hand-written code. Since the direct V&V of code generators is too laborious and complicated due to their complex (and often proprietary) nature, we have developed a generator plug-in to support the certification of the auto-generated code. Specifically, the AutoCert tool supports certification by formally verifying that the generated code is free of different safety violations, by constructing an independently verifiable certificate, and by explaining its analysis in a textual form suitable for code reviews. The generated documentation also contains substantial tracing information, allowing users to trace between model, code, documentation, and V&V artifacts. This enables missions to obtain assurance about the safety and reliability of the code without excessive manual V&V effort and, as a consequence, eases the acceptance of code generators in safety-critical contexts. The generation of explicit certificates and textual reports is particularly well-suited to supporting independent V&V. The primary contribution of this approach is the combination of human-friendly documentation with formal analysis. The key technical idea is to exploit the idiomatic nature of auto-generated code in order to automatically infer logical annotations. The annotation inference algorithm itself is generic, and parametrized with respect to a library of coding patterns that depend on the safety policies and the code generator. The patterns characterize the notions of definitions and uses that are specific to the given safety property. For example, for initialization safety, definitions correspond to variable initializations while uses are statements which read a variable, whereas for array bounds safety, definitions are the array declarations, while uses are statements which access an array variable. The inferred annotations are thus highly dependent on the actual program and the properties being proven. The annotations, themselves, need not be trusted, but are crucial to obtain the automatic formal verification of the safety properties without requiring access to the internals of the code generator. The approach has been applied to both in-house and commercial code generators, but is independent of the particular generator used. It is currently being adapted to flight code generated using MathWorks Real-Time Workshop, an automatic code generator that translates from Simulink/Stateflow models into embedded C code.

Denney, Ewen↗
DOE OSTI2026

ObstacleSense: Low-Power Neuromorphic Vision for Corridor Obstacle Awareness in Low-Level ADAS

The automotive industry’s pursuit of Level 5 autonomy is constrained by substantial perception-compute power requirements, often reaching 1, 000 + watts in full autonomy stacks. Reducing this energy burden requires rethinking perception not only at the high-end autonomy level, but also at the foundational Advanced Driver Assistance Systems (ADAS) level where low-power, safety-critical sensing can have broad impact. Neuromorphic vision provides a promising starting point: HD Dynamic Vision Sensors (DVS) can operate below 100 mW at the sensor level by reporting only asynchronous brightness changes. However, low-power sensing alone is insufficient if downstream perception reintroduces dense, energy-intensive computation. In particular, many event-driven object-detection pipelines still rely on CNN backbones, while purely spiking alternatives often trade away accuracy or ignore deployment constraints. We introduce ObstacleSense, a highly compact, CNN-free hybrid ANN–SNN framework for Level 0–1 forward-corridor obstacle awareness. Instead of performing full-scene object detection with a convolutional feature backbone, ObstacleSense targets the safety-critical question of whether the ego corridor is occupied and how far the nearest obstacle is. The architecture combines polarity-conditioned event encoding, lightweight temporal spiking dynamics, axial spatial mixing, and coarse-to-fine range estimation within a regular fixed-grid compute pattern. This design avoids the dense CNN backbone commonly used in event-based detection while maintaining a small state footprint suitable for eventual small-FPGA deployment. Before hardware mapping, we evaluate the software implementation using a model-side power proxy derived from MACs, weight and activation traffic, and spiking state updates under shared FP16 assumptions. On simulated CARLA event corpora, the deployment-oriented model achieves 0.9464 objectness F1, 0.9978 grid-level mAP, and 0.8987 m distance Mean Absolute Error at an estimated 1.92 mW proxy cost, while maintaining performance on unseen generalization test sequences.

Johnson-Scott, Zac [ORNL]↗