vault backup: 2025-08-11 16:31:54

Zettelkasten/Permanent Notes/thesis-ideas.md

@@ -183,45 +183,67 @@ manufacturing and other critical infrastructure.
 
 
 ### Related Papers:
+[[enhancing-cyber-physical-system-dependability-via-synthesis-challenges-and-future-directions]]
 ___________________________________________________________
 
 ## **Formally Verified Runtime Monitoring and Fallback**
 
 ### Goals:
 
-If this research is successful, we will be able to generate
-autonomous controller shields that provably adhere to specifications
-written with temporal logic.
+The goal of this research is to create a methodology for
+automatically generating runtime monitoring and fallback
+switching components from formal specifications in FRET for
+a reactor control system. Runtime monitoring with automatic
+switchover is a proven approach to ensuring safety in
+critical control systems: a primary controller operates
+under normal conditions, while a fallback safety controller
+is engaged if safety limits are approached or violated.
+These fallback mechanisms lend themselves naturally to
+linear temporal logic (LTL) specifications that can be
+elicited from high-level safety and operational requirements
+using automated tools. If the creation of these runtime
+monitors and switchovers can be automated from formal
+requirements, the engineering effort to implement robust
+fallback logic will be greatly reduced, while maintaining
+provable adherence to safety constraints. 
 
 ### Outcomes:
 
-- Create an intermediary shield that mediates signals between an
-  optimal control system and the physical plant (MODBUS)?
+1. Implement reactor control safety and operational
+   requirements as requirements in FRET, and extract
+temporal logic definitions of allowable system behaviors.
 
-- Translate specifications in a language like TLA+ into an
-executable program 
+2. Synthesize the switching component from LTL specification
+   using an automated tool such as Strix.
 
-- Provide proof artifacts that automatically generated
-shield components will not allow an arbitrary controller to
-reach an unsafe state.
+2. Develop a new endpoint for the Advanced Reactor Cyber
+   Analysis and Development Environment (ARCADE) that
+utilizes a shielding mechanism to switch between control
+trains.
+
+3. Create an example learning-based controller to
+   demonstrate the application of the machine generated
+shield.
+
+4. Provide proof artifacts that automatically generated
+   shield components will not allow an arbitrary controller
+to reach an unsafe state.
 
 ### Impact:
 
-Shielding is one of the preeminent ways to do safe machine
-learning controllers. Instead of putting the proof burden on
-the machine learning component, shielding creates a safe
-boundary in the state space where a safety controller will
-step in if the machine learning controller endangers the
-system. This technology solves a critical problem with high
-assurance systems: high assurance systems have critical
-safety requirements that make scrutiny on autonomous systems
-safety intense. Shielding can provide a safety barrier for
-the controller, allowing the architecture of the control
-laws to be amenable to more efficient machine learning based
-methods. Finally, utilizing an automatic translation from a
-temporal logic formulation of a speculation will allow the
-engineers of these systems to quickly and clearly implement
-a shield, without all of the cumbersome derivation.
+This approach addresses a persistent challenge in
+high-assurance systems: stringent safety requirements often
+force engineers to trade innovation and adaptability for
+proven but rigid safety mechanisms. The proposed method
+maintains safety guarantees while allowing more flexible or
+advanced primary control strategies. Moreover, automating
+the translation from formal safety requirements into
+executable monitoring and switchover logic creates a
+repeatable, transparent, and verifiable process. This
+reduces engineering effort, improves traceability to
+regulatory requirements, and may enable faster deployment of
+safety-critical control architectures in nuclear power and
+other critical infrastructure systems.
 
 ### Related Papers:
 
@@ -232,67 +254,67 @@ a shield, without all of the cumbersome derivation.
 ___________________________________________________________
 
 ## **Data-Driven Fault Detection Using High-Assurance Digital Twins** 
-(8)
 
 ### Goals:
 
-The goal of this research is to use machine learning to
-identify system faults of a reactor control system during
-runtime. A digital twin will be compared to measurements
-from a real plant to identify issues such as coolant losses,
-sensor and actuator failures, or component degredation so
-that safety strategic decisions about the plant can be made
-autonomously.
+The goal of this research is to develop a high-assurance,
+digital twin–based methodology for runtime fault detection
+in a reactor control system. A physics-based digital twin
+will be continuously compared with live plant measurements
+to detect anomalies such as coolant losses, sensor and
+actuator faults, and abnormal component degradation. Discrepancies
+between the digital twin and plant data will be analyzed
+using physics-informed machine learning models to diagnose
+the underlying fault and trigger appropriate autonomous
+control actions.
 
 ### Outcomes:
 
 For this research to be successful, I will accomplish the
 following:
 
-- Create a simulation suite for the Small Modular Advanced
-  High Temperature Reactor (SmAHTR) to simulate fault
-  conditions of sensors, actuators, and component degradation.
+1. Create a simulation suite for the Small Modular Advanced
+   High Temperature Reactor (SmAHTR) to simulate fault
+conditions including sensor and actuator failures, and
+component degradation.
 
-- Develop a physics informed neural network (PINN) approach
-  to evaluate physics discrepancies in measured signals and
-  to estimate physically relevant parameters to determine
-  real system divergence from the nominal plant. 
+2. Implement a physics-informed neural network (PINN)
+   framework to estimate key plant parameters, detect
+discrepancies between predicted and measured signals, and
+identify probable fault conditions.
 
-- Realize a proof of concept autonomous controller than can
-  react to fault conditions by switching to different
-control modes rather than only responding with reactor
-shutdown.
+3. Integrate the fault detection developed with a
+   proof-of-concept autonomous supervisory controller
+capable of implementing graded responses to fault
+conditions.
 
 ### Impact:
 
 The nuclear energy industry's largest expense is operations
-and maintenance (O&M). These costs include typical reactor repair
-and refueling, the labor involved to complete such
+and maintenance (O&M). These costs include typical reactor
+repair and refueling, the labor involved to complete such
 maintenance, and finally the labor involved in operating the
-reactor itself. Currently the largest of these O&M expenses
-is the labor and part cost used in maintenance, while large
-nuclear reactor facilities require a modest reactor operator
-budget per megawatt of energy produced. The advent of small
-modular reactors (SMRs) and microreactors (MRs) will change
-these economics significantly. 
+reactor itself. Large reactors are able to spread these O&M
+costs over large power outputs, but small modular reactors
+(SMR) and microreactors (MR) do not have the same capacity
+to dissipate O&M costs. Instead, SMRs and MRs must innovate
+in O&M to be economically competitve. As SMRs and MRs become
+more common, the cost of repair and maintenance will reduce
+dramatically as nuclear power components become modular,
+replaceable parts instead of the bespoke reactor designs
+currently operating in large reactors. Operator wages,
+however, can be expected to increase without introducing
+greater controller autonomy. SMRs and MRs have much smaller
+power output per reactor core, and if they are required to
+employ the same size reactor operator team as a conventional
+large reactor, will suffer from much larger operator expense
+per megawatt. Greater controller autonomy can solve this
+problem by unloading some reactor control responsibilities
+from the operator, and therein reduce labor cost.
 
-As SMRs and MRs become more common, the cost of repair and
-maintenance should reduce dramatically as nuclear power
-components will become modular, replaceable parts instead of
-the bespoke reactor designs currently operating. Operator
-wages, however, can be expected to increase without
-introducing greater controller autonomy. SMRs and MRs are
-much smaller output designs per reactor core, and if they
-are required to employ the same size reactor operator team
-as a conventional large reactor, will suffer from much
-larger operator expense per megawatt. Greater controller
-autonomy can solve this problem by unloading some reactor
-control responsibilities from the operator, and therein
-reduce labor consumption.
-
-<# TO DO #>
-Finally reactor safety can be improved by greater autonomy
-yada yada find some reasons to back this up.
+(I think something can be said about safety here too (time
+to respond, human factors removed, etc.), but I'm chewing on
+how to word that.)
 
 ### Related Papers:
 ___________________________________________________________