Auto sync: 2026-02-10 21:15:03 (1 files changed)

M  3-research-approach/v2.tex

3-research-approach/v2.tex

@@ -319,6 +319,91 @@ complex but deterministic behavior.
 
 % talk a bit about tools here like FRET. Talk about previous attempts.
 
+Human control of nuclear power can be divided into three different scopes:
+strategic, operational, and tactical. Strategic control is the high-level and
+long term decision making for the plant. This level has objectives that are
+complex and economic in scale, such as managing labor needs and supply chains to
+optimize sheduled maintenence and downtime. The time scale on this level of
+control is long, often over months or years. The lowest level of control is the
+tactical level. This is the individual control of pumps, turbines, and
+chemistry of the plant. This level of control has already been somewhat
+automated today in nuclear power, and is generally considered 'automatic
+control' when autonomous. These controls are almost always continuous systems,
+and have a direct impact on the physical state of the plant. Tactical control
+objectives are things like maintaining a pressurizer level, maintaining a
+certain core temperature, or adjusting reactivity with a chemical shim. The level of
+control linking these two levels, then, is the operational control scope.
+Operational control is the primary responsibility of human operators today.
+Operational control takes the current strategic objective, and implements
+tactical control objectives to drive the plant towards strategic goals. In this
+way, it is the bridge between high and low level goals. A strategic goal may be
+to perform refueling at a certain time, while the tactical level of the plant
+currently is focused on mainting a certain core temperature. The operational
+level is what issues the shutdown procedure of the plant, using several smaller
+tactical goals along the way to achieve this objective. Thus, the combination of
+the operational and tactical level of the plant fundamentally forms a hybrid
+controller. The tactical level is the continuous evolution of the plant
+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
 
 % The whole point of a hybrid system is that there are continuous components