3-research-approach/v2.tex

@@ -319,91 +319,6 @@ 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