From 54f0f2f1e5769e1db355490dfa94088508897463 Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 16 Mar 2026 13:53:24 -0400 Subject: [PATCH] Edit Research Statement: address DAS+Split comments with oldt/newt markup --- 1-goals-and-outcomes/research-statement.tex | 164 ++++++++++---------- 1 file changed, 79 insertions(+), 85 deletions(-) diff --git a/1-goals-and-outcomes/research-statement.tex b/1-goals-and-outcomes/research-statement.tex index 74f139f..feb0c29 100644 --- a/1-goals-and-outcomes/research-statement.tex +++ b/1-goals-and-outcomes/research-statement.tex @@ -1,108 +1,102 @@ % GOAL PARAGRAPH The goal of this research is to develop a methodology for creating autonomous -control systems with event-driven control laws that have guarantees of safe and -correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.} +\oldt{control systems with event-driven control laws that have guarantees of +safe and correct behavior.} \newt{hybrid control systems with mathematical +guarantees of safe and correct behavior.}\splitnote{Strong, direct opening. +Sets scope immediately.} \dasinline{Title needs updated to High Assurance Hybrid Control Systems. Maybe removal of `formal'?} % INTRODUCTORY PARAGRAPH Hook Nuclear power relies on extensively trained operators who follow detailed -written procedures to manage reactor control.\dasinline{Why is there any -hyphenation at all? Why not full justification?} Based on these procedures and -\oldt{operators'} \newt{their} interpretation of plant conditions, \oldt{operators} \newt{they} make critical decisions -about when to switch between control objectives. -\splitinline{Consider: ``operators'' appears 3x in two sentences. Maybe: -``Based on these procedures and their interpretation of plant conditions, -they make critical decisions...''} +written procedures to manage reactor control. Based on these procedures and +\oldt{operators'} \newt{their} interpretation of plant conditions, +\oldt{operators} \newt{they} make critical decisions about when to switch +between control objectives. % Gap -\oldt{But, reliance} \newt{This reliance} on human operators has created an economic challenge for -next-generation nuclear power plants. -\splitinline{``But, reliance'' — the comma after ``But'' is unusual. Either -drop it or restructure: ``However, this reliance...'' or ``This reliance, -however, has created...''} -\dasinline{Or just straight up ``this reliance''. -Right to the topic.} -Small modular reactors face significantly higher per-megawatt staffing costs -than conventional -plants.\dasinline{Obvious but source required.} Autonomous control systems \oldt{are -needed that can} \newt{must} safely manage complex -operational sequences with the same assurance as human-operated systems, but +\oldt{But, reliance} \newt{This reliance} on human operators has created an +economic challenge for next-generation nuclear power plants. Small modular +reactors face significantly higher per-megawatt staffing costs than +conventional plants.\dasinline{Obvious but source required.} Autonomous +control systems \oldt{are needed that can} \newt{must} safely manage complex +operational sequences with the same assurance as human-operated systems, but without constant supervision. -\splitinline{``are needed that can'' --- passive. Try: ``Autonomous control -systems must safely manage...''} % APPROACH PARAGRAPH Solution -To address this need, we will combine formal methods from computer science with -control theory to build hybrid control systems that are correct by -construction.\splitnote{Clear statement of approach.}\dasinline{Add -``and leverage existing domain knowledge'' or similar. -Industry knowledge can be reused here --- less like -starting from scratch.} +To address this need, we will combine formal methods from computer science +with control theory \oldt{to build hybrid control systems that are correct by +construction.} \newt{to build hybrid control systems that are correct by +construction, leveraging the extensive domain knowledge already embedded in +existing operating procedures and safety analyses.} % Rationale Hybrid systems use discrete logic to switch between continuous control modes, similar to how operators change control strategies. Existing formal methods -generate provably correct switching logic but cannot handle continuous dynamics -during transitions, while traditional control theory verifies continuous -behavior but lacks tools for proving discrete switching +generate provably correct switching logic but cannot handle continuous +dynamics during transitions, while traditional control theory verifies +continuous behavior but lacks tools for proving discrete switching correctness.\splitnote{Nice parallel structure showing the gap.} + % Hypothesis and Technical Approach We will bridge this gap through a three-stage methodology. First, we will -translate written operating procedures into temporal logic specifications using -NASA's Formal Requirements Elicitation Tool (FRET), which structures -requirements into scope, condition, component, timing, and response elements. -This structured approach enables realizability checking to identify conflicts -and ambiguities in procedures before -implementation.\dasinline{Had to read this twice.} Second, we will synthesize -discrete mode switching logic using reactive -synthesis\dasinline{Also had to read this twice. A lot of +translate written operating procedures into temporal logic specifications +using NASA's Formal Requirements Elicitation Tool (FRET). \oldt{which +structures requirements into scope, condition, component, timing, and +response elements. This structured approach enables realizability checking to +identify conflicts and ambiguities in procedures before implementation.} +\newt{FRET structures requirements into scope, condition, component, timing, +and response elements, enabling realizability checking that identifies +conflicts and ambiguities in procedures before implementation.} +\dasinline{Had to read this twice.} +Second, we will synthesize discrete mode switching logic using reactive +synthesis \oldt{to generate deterministic automata that are provably correct +by construction.} \newt{to produce deterministic automata that are correct by +construction.}\dasinline{Also had to read this twice. A lot of jargon. Check topic stress.} -to generate deterministic automata that are provably -correct by construction. Third, we will develop continuous -controllers for each discrete mode using standard control theory and -reachability analysis. We will classify continuous modes based on their -transition objectives, and then employ assume-guarantee contracts\dasinline{I don't think -I ever mention this phrase again specifically. Might be a -dogwhistle to other work unintentionally. Must be -careful.} and barrier -certificates to prove that mode transitions occur safely and as defined by the -deterministic automata. This compositional approach enables local verification -of continuous modes without requiring global trajectory analysis across the -entire hybrid system. We will demonstrate this on an Emerson Ovation control -system.\dasinline{Where did this come from? Needs context.} -\splitinline{This paragraph is dense. Consider breaking after the three -stages, then a new paragraph for the compositional verification point and -Emerson demo.} +Third, we will develop continuous controllers for each discrete mode using +standard control theory and reachability analysis. We will classify +continuous modes based on their transition objectives \oldt{, and then employ +assume-guarantee contracts and barrier certificates to prove that mode +transitions occur safely and as defined by the deterministic automata.} +\newt{and verify safe mode transitions using barrier certificates and +reachability analysis.}\dasinline{I don't think I ever mention this phrase +again specifically. Might be a dogwhistle to other work unintentionally. Must +be careful.} + +This compositional approach enables local verification of continuous modes +without requiring global trajectory analysis across the entire hybrid system. +\oldt{We will demonstrate this on an Emerson Ovation control system.} +\newt{We will validate this methodology through hardware-in-the-loop testing +on an Emerson Ovation distributed control system, made possible through the +University of Pittsburgh Cyber Energy Center's industry partnership.} +\dasinline{Where did this come from? Needs context.} + % Pay-off -This approach \oldt{will demonstrate autonomous control can be used for} \newt{enables autonomous management of} complex -nuclear power operations while maintaining safety -guarantees. -\splitinline{``can be used for'' — weak. Try: ``...will demonstrate that -autonomous control can manage complex nuclear power operations while -maintaining safety guarantees.'' Or even stronger: ``...enables autonomous -management of complex nuclear power operations with safety guarantees.''} +This approach \oldt{will demonstrate autonomous control can be used for} +\newt{enables autonomous management of} complex nuclear power operations +while maintaining safety guarantees. % OUTCOMES PARAGRAPHS If this research is successful, we will be able to do the following: \begin{enumerate} % OUTCOME 1 Title - \item \textit{Synthesize written procedures into verified control logic.} + \item \textit{Synthesize written procedures into verified control logic.} % Strategy We will develop a methodology for converting written operating procedures into formal specifications. These specifications will be synthesized into - discrete control logic using reactive synthesis tools. + discrete control logic using reactive synthesis tools. % Outcome - Control engineers will be able to generate mode-switching controllers from - regulatory procedures with little formal methods - expertise,\dasinline{This may not be true, and perhaps - does not belong.} reducing - barriers to high-assurance control - systems.\splitnote{Good practical framing --- emphasizes accessibility.} + \oldt{Control engineers will be able to generate mode-switching + controllers from regulatory procedures with little formal methods + expertise, reducing barriers to high-assurance control systems.} + \newt{This will reduce barriers to high-assurance control systems by + generating verified mode-switching controllers directly from regulatory + procedures.}\dasinline{This may not be true, and perhaps does not belong.} % OUTCOME 2 Title - \item \textit{Verify continuous control behavior across mode transitions. } + \item \textit{Verify continuous control behavior across mode transitions.} % Strategy - We will develop methods using reachability analysis to ensure continuous - control modes satisfy discrete transition requirements. + We will develop methods using reachability analysis to ensure continuous + control modes satisfy discrete transition requirements. % Outcome Engineers will be able to design continuous controllers using standard practices while ensuring system correctness and proving mode transitions @@ -110,18 +104,18 @@ If this research is successful, we will be able to do the following: % OUTCOME 3 Title \item \textit{Demonstrate autonomous reactor startup control with safety - guarantees. } + guarantees.} % Strategy We will implement this methodology on a small modular reactor simulation - using industry-standard control hardware. % Outcome - Control engineers will be able to \oldt{implement high-assurance autonomous - controls on industrial platforms they already use, enabling users to - achieve autonomy without retraining costs or developing new - equipment.} \newt{achieve autonomy without retraining costs or developing new equipment by implementing high-assurance autonomous controls on industrial platforms they already use.}\splitnote{Strong industrial grounding --- the ``platforms they - already use'' point is compelling for - adoption.}\dasinline{Flip the clauses. Put retraining - and new equipment before the comma, end with building - HAHACs with control hardware they already use. - That's the more important part.} + using industry-standard control hardware. + % Outcome + \oldt{Control engineers will be able to achieve autonomy without + retraining costs or developing new equipment by implementing + high-assurance autonomous controls on industrial platforms they already + use.} \newt{Without retraining costs or new equipment, control engineers + will be able to implement high-assurance autonomous controls on industrial + platforms they already use.}\dasinline{Flip the clauses. Put retraining + and new equipment before the comma, end with building HAHACs with control + hardware they already use. That's the more important part.} \end{enumerate}