This paper introduces a procedure to prove the safety of large-scale nonlinear hybrid systems. Critical systems are prone to vulnerabilities due to increased complexity. Formal methods for hybrid systems struggle with the computational issues of continuous dynamics and identifying invariants for nonlinear theorem proving. We propose an approach that integrates multiple formal verification methods for hybrid systems. This approach uses reachability analysis and differential dynamic logic to model and verify the safety of critical systems. By decomposing the system into components, our approach reduces computational load, enhancing the formal verification process of critical systems against potential hazards. This approach offers a comprehensive framework for the safety of complex critical systems.

Medical device security lies at the intersection of healthcare, technology, and cybersecurity and involves protecting medical devices, related data, and patients from cyberattacks. Medical devices includes everything from large clinic-based machines like MRIs to small devices like insulin pumps and pacemakers. A primary challenge arises from the increasing numbers of these devices that are network-connected. This connectivity enables benefits of remote monitoring and control, improved data collection and diagnostics, and personalized treatments; but, it also introduces new cybersecurity risks. A single software failure, bug, or attack in a complex, monolithic system can cascade and risk patient safety.

This paper presents research that integrates condition monitoring and prognostics with decision making for nuclear power plant operations and maintenance aimed at reducing lifetime maintenance and repair costs. Additionally, a focal point of this research is to make the decisions explainable to operators, improving the trustworthiness of the decisions from what can be considered a black box model. In this work, we develop and evaluate an explainable, online asset management methodology to help reduce lifetime maintenance and repair costs. Using the latest advancements in condition monitoring, inventory management, deep reinforcement learning, and explainable artificial intelligence methods, we create a predictive maintenance methodology that can optimize the maintenance and spare part management of a repairable nuclear power plant system.To demonstrate these methods, preliminary studies were conducted on a representative maintenance system undergoing a stochastic degradation process that requires repairs or replacement to continue operation. Using deep reinforcement learning, we were able to reduce maintenance spending by approximately 50% compared to optimized, time-based maintenance strategies for the chosen system. A key component of our methodology is the integration of Shapley values to quantify the contribution of various factors to the decision-making process. This addition enhances the explainability and trustworthiness of our decisions, providing operators with transparent and understandable insights into the rationale behind maintenance strategies. The robustness and resiliency of our decision policy against observation noise were also thoroughly evaluated, demonstrating its effectiveness in uncertain operational environments.

This paper discusses methods to prove the safety of critical cyber-physical systems. Critical infrastructure, such as nuclear power plants, are prone to vulnerabilities due to the integration of industrial internet-of-things technologies. Automation and computation introduces greater complexity into these systems. Thus, traditional safety analysis methods, including probabilistic risk assessment and system theoretic process analysis, can be limited in their scope of analysis, specifically in addressing software vulnerabilities and the cyber-physical interface. To address these limitations, we propose an approach to safety analysis by integrating multiple formal verification methods within the context of hybrid systems. This approach employs a combination of reachability analysis and theorem proving, specifically using differential dynamic logic (dL), to model and verify the safety of a nuclear plant's thermal dispatch operation. By decomposing the system into individual components, our method reduces computational complexity and enhances the verification process, ensuring the resiliency of critical infrastructure against potential hazards. This integrated approach offers a comprehensive framework for the safety and security of complex, cyber-physical systems.

Cyber-physical systems (CPSs) require reliable, safe, and secure control of critical infrastructure, combining computational and networking capabilities, which heighten the risk of cyberattacks. These attacks can disrupt the physical process, causing unforeseen consequences. One solution is using fully homomorphic encryption (FHE) to protect the control loop, allowing for secure computations and communications without compromising signal and control system privacy. One challenge with FHE, however, is its requirement for inputs to be integers. This paper introduces a modified FHE scheme based on the learning with errors (LWE) problem. Our proposed scheme leverages a generalized LWE encoding function and modifies the Gentry-Sahai-Waters (GSW) gadget decomposition tool to encrypt the control system. Using the modified LWE scheme, we formalize a fully encrypted control system, supported by simulated results.

Molecular motors employ chemical energy to generate unidirectional mechanical output against a track while navigating a chaotic cellular environment, potential disorder on the track, and against Brownian motion. Nevertheless, decades of nanometer-precise optical studies suggest that myosin-5a, one of the prototypical molecular motors, takes uniform steps spanning 13 subunits (36 nm) along its F-actin track. Here, we use high-resolution interferometric scattering microscopy to reveal that myosin takes strides spanning 22 to 34 actin subunits, despite walking straight along the helical actin filament. We show that cumulative angular disorder in F-actin accounts for the observed proportion of each stride length, akin to crossing a river on variably spaced stepping stones. Electron microscopy revealed the structure of the stepping molecule. Our results indicate that both motor and track are soft materials that can adapt to function in complex cellular conditions.

The nuclear industry’s economic viability is challenged by significant operations and maintenance (O&M) costs. Although maintenance strategies are often risk-averse, many maintenance programs rely on schedule-based strategies that perform repairs and replacements regardless of the asset’s condition, leading to unnecessary repairs and high costs. Predictive maintenance can help alleviate these costs through condition monitoring and risk-informed decision-making. In this article, we show that the use of improved reliability models can help reduce the total cost of ownership (TCO) for a high-value repairable asset. Current risk-informed methods used in the industry today rely on mean-time-between-failure (MTBF) models that may oversimplify failure likelihood estimation. Improvements can be made by integrating condition monitoring, operational history, and maintenance effectiveness into a hybrid reliability model. In contrast with conventional MTBF methods, the generalized renewal process uses recurrent event analysis and historical repair data to quantify the effectiveness of maintenance repairs and estimate the likelihood of failure. During a case study on a nuclear power plant’s circulating water system, a hybrid reliability model was fitted to the historical data and shown to have improved likelihood estimations when compared to a MTBF model. Monte Carlo simulations were then used to simulate and compare TCO for various maintenance strategies, showing that an extended replacement interval can reduce overall costs by upwards of 10.7%. The successful results of the improved reliability models showcase the ability to aid decision-making and reduce overall operations and maintenance costs in the nuclear power industry.

To improve the viability of nuclear power plants, there is a need to reduce their operational costs. Operational costs account for a significant portion of a plant’s yearly budget, due to their scheduled-based maintenance approach. In order to reduce these costs, proactive methods are required that estimate and forecast the state of a machine in real time to optimize maintenance schedules. In this research, we use Bayesian networks to develop a framework that can forecast the remaining useful life of a centrifugal pump. To do so, we integrate survival analysis with Bayesian statistics to forecast the health of the pump conditional to its current state. We complete our research by successfully using the Bayesian network on a case study. This solution provides an informed probabilistic viewpoint of the pumping system for the purpose of predictive maintenance.

Myosin-5a is a molecular motor that transport cargoes and steps in a symmetric hand-over-hand mechanism along actin, with both heads attached most of the time. By tracking 20 nm gold nanoparticles attached to a single head of the myosin-5a heavy meromyosin-like construct, with sub-nanometer precision via interferometric scattering (iSCAT) microscopy, analysis of stride-sizes showed peaks corresponding to 22, 24, 26, 28, 30, 32 and 34 actin subunits. Kinetic analysis of dwell times determined for different stride sizes at limiting [ATP] showed changes in the ADP release rate for azimuthally strained myosin-5a.

Total internal reflection fluorescence microscopy can detect and image single fluorescently labeled molecules close to a surface with high temporal and spatial resolution. Despite the high specificity introduced by the fluorescent label, it is not universal, and label must be attached to individual proteins through genetic engineering or designed antibodies. Mass photometry (MP) interferometrically detects elastic scattering rather than fluorescence of particles landing at a glass-water interface, enabling not only detection, imaging and localization, but also the mass measurements of single proteins. MP, however, struggles with detecting species of low molecular mass (< 40 kDa) and its non-specificity prevents particles of similar mass to be distinguished solely by the one-dimensional scattering readout. Here, we report on the combination of single molecule fluorescence and scattering microscopy. We simultaneously record the position of a particle in time and space via fluorescence and determine its mass via elastic scattering to improve the sensitivity and specificity of mass photometry. Firstly, we used a range of proteins tagged with green fluorescent protein (GFP), and separated landing events into fluorescent and non-fluorescent species which suppresses noise at the lower end of the resulting mass distribution and enables quantification of the labeling efficiency. Secondly, we investigated protein-protein interactions where only one of the binding partners was fluorescently labeled with GFP. The separation into fluorescent and non-fluorescent events enabled us to separately determine the mass of two species with an improved precision much like 2D spectroscopy. The enhanced specificity allows differentiation of stoichiometries between binding partners which were otherwise indistinguishable based on the scattering contrast alone.

This work-in-progress paper proposes a design methodology that addresses the complexity and heterogeneity of cyber-physical systems (CPS) while simultaneously proving resilient control logic and security properties. The design methodology involves a formal methods-based approach by translating the complex control logic and security properties of a water flow CPS into timed automata. Timed automata are a formal model that describes system behaviors and properties using mathematics-based logic languages with precision. Due to the semantics that are used in developing the formal models, verification techniques, such as theorem proving and model checking, are used to mathematically prove the specifications and security properties of the CPS. This work-in-progress paper aims to highlight the need for formalizing plant models by creating a timed automata of the physical portions of the water flow CPS. Extending the time automata with control logic, network security, and privacy control processes is investigated. The final model will be formally verified to prove the design specifications of the water flow CPS to ensure efficacy and security.

Many modern critical infrastructures are cyber-physical systems that rely on the integration of physical processes and computational resources. While this integration enables advanced system diagnostics, monitoring, and control, it also exposes the physical process to cyber-threats. Critical infrastructures such as nuclear power plants may be targeted by a variety of threat agents, each with unique motivations, resources, and capabilities. A Bayesian game-theoretic approach is presented to secure critical infrastructure when the adversary's characteristics are uncertain. In a Bayesian game, some players have incomplete information about the other players. Within the context of critical infrastructure cybersecurity, plant defenders have incomplete information about threat agents, and threat agents have incomplete information about plant defenders. A Bayesian game provides a quantitative method for security teams to identify optimal defense strategies. The Bayesian game-theoretic approach is demonstrated on the residual heat removal system of a boiling water reactor. Threat agents are modeled as types in the game using a threat agent library that defines each threat's characteristics. Similarly, different types of defenders are modeled by considering consequences of importance to plant stakeholders. Using these type definitions, utility functions are defined for each player. Nash equilibria of the Stackelberg game and two simultaneous games are identified and discussed. Using this procedure, a security team at a nuclear power plant can select the optimal strategy to defend the plant from cyber-threats.

Protein assembly is a main route to generating complexity in living systems. Revealing the relevant molecular details is challenging because of the intrinsic heterogeneity of species ranging from few to hundreds of molecules. Here, we use mass photometry to quantify and monitor the full range of actin oligomers during polymerization with single-molecule sensitivity. We find that traditional nucleation-based models cannot account for the observed distributions of actin oligomers. Instead, the key step of filament formation is a slow transition between distinct states of an actin filament mediated by cation exchange or ATP hydrolysis. The resulting model reproduces important aspects of actin polymerization, such as the critical concentration for filament formation and bulk growth behavior. Our results revise the mechanism of actin nucleation, shed light on the role and function of actin-associated proteins, and introduce a general and quantitative means to studying protein assembly at the molecular level.

To facilitate the automated online monitoring of power plants, a systematic and qualitative strategy for anomaly detection is presented. This strategy is essential to provide credible reasoning on why and when an empirical versus hybrid (i.e., physics-supported) approach should be used and to determine the ideal mix of these two approaches for a defined anomaly detection scope. Empirical methods are usually based on pattern, statistical, and causal inference. Hybrid methods include the use of physics models to train and test data methods, reduce data dimensionality, reduce data-model complexity, augment data, and reduce empirical uncertainty; hybrid methods also include the use of data to tune physics models. The presented strategy is driven by key decision points related to data relevance, simple modeling feasibility, data inference, physics-modeling value, data dimensionality, physics knowledge, method of validation, performance, data availability, and suitability for training and testing, cause-effect, entropy inference, and model fitting. The strategy is demonstrated through a pilot use case for the application of anomaly detection to capture a valve packing leak at the high-pressure coolant injection system of a nuclear power plant.

Single particle tracking has found broad applications in the life and physical sciences, enabling the observation and characterization of nano- and microscopic motion. Fluorescence-based approaches are ideally suited for high-background environments, such as tracking lipids or proteins in or on cells, due to superior background rejection. Scattering-based detection is preferable when localization precision and imaging speed are paramount due to the in principle infinite photon budget. Here, we show that micromirror-based total internal reflection dark field microscopy enables background suppression previously only reported for interferometric scattering microscopy, resulting in nanometer localization precision at 6 μs exposure time for 20 nm gold nanoparticles with a 25 × 25 μm2 field of view. We demonstrate the capabilities of our implementation by characterizing sub-nanometer deterministic flows of 20 nm gold nanoparticles at liquid-liquid interfaces. Our results approach the optimal combination of background suppression, localization precision, and temporal resolution achievable with pure scattering-based imaging and tracking of nanoparticles at interfaces.

This paper develops an automated fault detection tool to detect very small LOCAs in pressurized water reactors that would be difficult for operators to detect manually. One of the primary challenges with previous automated fault detection methods, which are data-driven, is that they require data from LOCAs; however, it may be difficult to capture real operational data from LOCA scenarios. This work uses a physics-inspired approach that equates the physical effects of a LOCA to changes in known variables. This approach enables the detection of very small LOCAs using data-driven approaches that use nominal operating data without the need for LOCA data. The approach combines data-driven modeling with control-theoretic estimation techniques to detect LOCAs and estimate their magnitudes in real-time. First, simulated process data for a variety of nominal operating conditions is collected using a generic pressurized water reactor simulator. Then, that data is used to train an artificial neural network regression model that captures the nonlinear plant dynamics. Finally, the regression model is used in a particle filter to detect the onset and estimate the magnitude of the leak. These methods are successfully verified using LOCA simulations that would be hard to manually distinguish from normal operating transients.

Cyber-physical systems are engineered systems that rely on the integration of physical processes and computational resources. While this integration enables advanced techniques for monitoring and controlling systems, it also exposes the physical process to cyber-threats. An attacker who is able to access control inputs and mask measurements could damage the system while remaining undetected. By masking certain measurement signals, an attacker may be able to render a portion of the state space unobservable, meaning that it is impossible to estimate or infer the value of those states. This is called an observability attack. A game-theoretic approach is presented to analyze observability attacks. The attacker's strategy set includes all possible combinations of masked measurements. The defender's strategy set includes all possible combinations of measurement reinforcements. The attacker's and defender's utilities are quantified using the responses of the observable and unobservable states. The observability attack game is analyzed for a nuclear balance of plant system. Multiple pure-strategy and mixed-strategy Nash equilibria are identified, and the conditions for their existence are presented. Using this procedure, a security and control engineer can select the optimal strategy to defend a cyber-physical system from observability attacks.

A zero-dynamics attack allows an attacker to input some control action that results in zero measurable output but nonzero response of the internal states. This paper extends previous works on zero-dynamics attacks to nonlinear system dynamics. This is accomplished using invariant subspace techniques that identify the subspace on which zero dynamics exist. An iterative algorithm is presented to identify both this subspace and the resulting zero dynamics of the system. These methods are implemented on a model of a pressurizer in a nuclear power plant, which is a critical subsystem of pressurized water reactors that monitors and controls the system pressure and coolant inventory. This implementation is done by analyzing all combinations of attackable signals. These attackable signals are the set of all system inputs and outputs. From this analysis, there are eight unique combinations of attacked actuators and sensors that result in zero-dynamics attacks. These combinations are characterized by stability and damage time, where damage time is the time it takes to reach some undesirable state. The damage times range from half a day to sixteen days, depending on the number of signals the attacker has access to. These results demonstrate that the physics of the pressurizer system creates some vulnerabilities to zero-dynamics attacks. This work provides plant designers with tools to identify which subsystems are most susceptible to zero-dynamics attacks and might require additional defenses.

This work uses probabilistic robustness techniques to show how the stability margin of an uncertain controlled structure that operates in a harsh, potentially radioactive environment can be analyzed in order to find a less conservative destabilizing uncertainty perturbation. The uncertainty is quantified in terms of a measure on the size of the covariance matrix in a multivariate Gaussian distribution. This uncertainty is used to capture the aggregate effects on a structure’s dynamic behavior due to material changes resulting from radiation embrittlement and mechanical fatigue. A probabilistic-robust full-state feedback \({\mathcal {H}_\infty }\) controller is synthesized for a low-dimensional structural model using a technique known as scenario-based probabilistic-robust synthesis. A probabilistic-robust stability margin is defined and extracted from a stability degradation function, demonstrating that a fourfold increase in the amount of uncertainty in the model can be tolerated if the designer is willing to concede a small probability that the actively-controlled structure may be unstable for certain system configurations.