From 28091b89a98488c6547564c2aba98bb0a1bec9a4 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 10 Feb 2026 21:15:03 -0500 Subject: [PATCH] Auto sync: 2026-02-10 21:15:03 (1 files changed) M 3-research-approach/v2.tex --- 3-research-approach/v2.tex | 55 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/3-research-approach/v2.tex b/3-research-approach/v2.tex index 21aa7d2..16a89c1 100644 --- a/3-research-approach/v2.tex +++ b/3-research-approach/v2.tex @@ -347,7 +347,62 @@ according to the control input and control law, while the operational level is a discrete state evolution which determines the tactical control law to reach different operational states. +This operational control level is the main reason for the requirement of human +opeartors in nuclear control today. The hybrid nature of this control system +makes it difficult to prove that a controller will perform according to the +strategic requirements, as the infrastructure to build hybrid systems today +dooes not exist. Humans have been used for this layer because the general +intelleigence of humans has be relied upon as a safe way to manage the hybrid +nature of this system. But, these operators are using prescriptive operating +manuals to perform their control with strict procedures on what control to +implement at a given time. These procedures are the key to the operational +control scope. +The method of constructing a HAHACS in this proposal leverages two key points of +the way this control scope is done today: first, the operational scope control +is effectively discrete control. Second, the rules of implementing this control +are described a priori to their implementation in operating procedures. We can +make great use of these facts by formalizing the rules for transitioning between +discrete states. To do this, we will use temporal logic to formalize discrete +switching behavior. + +Temporal logic is a rich syntax that allows for the definition of logical +calculations including time related bounds. For this reason, we can make +statements relating discrete control modes to one another. Using temporal logic, +we can effectively describe all of the requirements of a HAHACS. The guard +conditions \(G\) are easily defined by determining boundary conditions between +discrete states and defining their behavior, while continuous mode invariants +can be defined using temporal logic statements as well. These form the basis of +any proofs about a HAHACS, and are the fundamental 'truth' statements about what +the behavior of the system is designed to be. + +To build these temporal logic statements, an intermediary tool called FRET is +planned to be used. FRET stands for Formal Requirements Elicitation Tool, and +was designed by NASA to build high assurance timed systems. FRET is an +intermediarly language between temporal logic and natural language that allows +for rigid definitions of temporal behvarior while using a logic-novice friendly +syntax. This benefit is crucial for the feasibility of this methodology for +industry, as minimizing the barrier to formal methods is a critical component of +their scucess. By reducing the expert knowledge required to use these tools, +their adoption with current workforce becomes easier. + +A key feature of FRET is the ability to start with logically imprecise +statements and consecutively refine them into a well-posited specification. We +can use this to our advantage by directly dumping in operating procedures and +design requirements into FRET in natural language, and iteratively refining them +into the specifications for a HAHACS. This has two distinct but important +benefits. First, it allows us to draw a direct link from the design +documentation to the digital system implementation. Second, it clearly +demonstrates where the natural language documents are insufficient. These +procedures may still be used by human operators, so any wiggle room for +interpretation is a weakness that must be addressed. + +%Talk about how we go from temp logic to reactive synth. Metnion fret can +%export, or naturlly support reactive synth solver ltlsynt, a sota react synth +%solver + +% talk about what the benefits of reactive synth are. Proof chain, machine +% checkable, blah blah blah %%%%%%%%%%%% Building continuous controllers