A Typing Discipline for High-Assurance Control Systems

Taylor, Max

Home/Archive/DOE OSTI

DOE OSTI · 3021464

A Typing Discipline for High-Assurance Control Systems

Taylor, Max

View original source ↗Read source document ↗Export metadata ↓

Abstract

This poster describes a typing discipline for high-assurance industrial systems based on three novel type systems. The first type system, information flow control (IFC), controls the flow of data through the system. The second system, dependent session types, restricts messages exchanged during the execution of a communication protocol to avoid dangerous states. The third system uses dimensional analysis to avoid subtle bugs that adversaries can exploit to cause the system to enter a dangerous state. This poster describes how a combination of these approaches can prevent sophisticated cyber attacks, such as the infamous Stuxnet incident, from occurring. In addition, we provide experimental evidence to support the claim that these approaches can be applied in control systems that are resource-constrained.

Explore related subjects

42 - ENGINEERING 97 - MATHEMATICS AND COMPUTING control systems critical infrastructure type theory

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Taylor, Max. 2024-07-22. A Typing Discipline for High-Assurance Control Systems. https://www.osti.gov/biblio/3021464

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

DOE OSTI2026

Simulating Thermoelectric Devices Using the MOOSE Framework

Thermoelectric generators (TEG) are devices that generate energy by converting heat into electricity or provide cooling via the Peltier effect. This feature of thermoelectric devices originates from the Seebeck, Peltier, Thomson, and Joule heating effects. TEGs can be applied in energy and thermal management systems such as waste heat recovery and refrigeration, respectively. Thermoelectric device design is influenced by the material selection and the device's geometry operating conditions. Therefore, predicting, verifying, and validating thermoelectric device performance using simulations tools is essential to deploying thermoelectric devices in industry. The Multiphysics Object-Oriented Simulation Environment (MOOSE) Framework is an open-source simulation tool capable of modeling simple to complex systems. In this work, we demonstrate MOOSE's thermoelectric device modeling capabilities by simulating a unicouple, module, and exhaust gas recovery system. The Seebeck, Peltier, Thomson, and Joule heating physics are implemented into MOOSE. The MOOSE thermoelectric physics were thoroughly verified and validated using published COMSOL® results and experimental data. In addition, thermoelectric modules were integrated into an exhaust gas recovery system using the MOOSE MultiApp function as a demonstration of the model's ability. The verification and validation results and exhaust gas heat recovery system showcases MOOSE's capability to model thermoelectric devices and integrate these devices into practical energy systems.

42 - ENGINEERING↗

DOE OSTI2026

Validation of OpenPronghorn for Periodic Hill Flow Separation

OpenPronghorn is an open-source, MOOSE-based thermal-hydraulics simulation tool used for advanced reactor analysis. As an open-source code, it offers a transparent framework for validating governing equations, assumptions, and numerical methods against established benchmarks. This study evaluates OpenPronghorn's RANS turbulence model against the ERCOFTAC Case 81 periodic hill benchmark, a standard test case for separated turbulent flow featuring curved-wall separation, recirculation, shear-layer development, and reattachment. Streamwise velocity profiles predicted by OpenPronghorn were compared to reference LES data at multiple x/h locations. Results show that OpenPronghorn captures the overall trend of the velocity profiles, but the largest discrepancies occur in the separated-flow region, where turbulence is highly anisotropic and strongly affected by adverse pressure gradients and wall curvature—conditions that are inherently difficult for standard RANS models to resolve. Future work will test alternative k-e model variants and correction terms to improve prediction accuracy in this region.

42 - ENGINEERING↗

DOE OSTI2026

XAFS Analysis Report

X-ray absorption spectroscopy (XAS) measurements were performed using a laboratory-based easyXAFS 300+ spectrometer. The XAFS data shows predominantly metallic phases.

42 - ENGINEERING↗