Split: cleanup preliminary results - fix typos, add PKE/thermal-hydraulic/reactivity equations with labels, reformat placeholders as proper dasnotes, reference earlier reachability formalism

3-research-approach/approach.tex

@@ -591,60 +591,108 @@ analysis).}
 In order to demonstrate the feasibility of this research proposal, we applied
 this approach to HAHACS creation to a simple nuclear reactor model, with limited
 procedural guidance. We created a simple point kinetics reactor model with
-a two-node thermal hydraulics model. The reactor assumes plant parametrs and
+a two-node thermal hydraulics model. The reactor assumes plant parameters and
-mateiral properties cosistent with a Uranium-235 pressurized water reactor. For
+material properties consistent with a Uranium-235 pressurized water reactor. For
-teh reactor core, six precursor groups are included, and fuel temperature and
+the reactor core, six precursor groups are included, and fuel temperature and
 moderator temperature feedback are implemented. For the thermal hydraulics,
 basic convection assumptions are made about the heat generated from the fuel's
 reactivity, while the coolant is assumed to be single phase water. The
 differential equations representing each part of the system are described as
-follows:
+follows.
 
+The point kinetics equations with delayed neutron precursors govern the
+neutron population $n(t)$ and precursor concentrations $C_i(t)$:
+%
 \begin{equation}
-  %PKE with precursors and temperature effects
+  \frac{dn}{dt} = \frac{\rho(t) - \beta}{\Lambda} n(t)
-  \label{eq:PKE}
+    + \sum_{i=1}^{6} \lambda_i C_i(t)
+  \label{eq:pke}
 \end{equation}
-
+%
 \begin{equation}
-  %thermal hydraulics
+  \frac{dC_i}{dt} = \frac{\beta_i}{\Lambda} n(t) - \lambda_i C_i(t),
-  \label{eq:thermal_hyrdaulics}
+  \quad i = 1, \ldots, 6
+  \label{eq:precursors}
 \end{equation}
+%
+where $\rho$ is the total reactivity, $\beta = \sum \beta_i$ is the total
+delayed neutron fraction, $\Lambda$ is the prompt neutron generation time,
+$\lambda_i$ are the precursor decay constants, and $\beta_i$ are the
+individual group delayed neutron fractions.
 
-Reactivity meanwhile is a sum of several different sources. First, reactivity is
+The two-node thermal hydraulics model couples fuel temperature $T_f$ and
-a factor of the fuel itself. Second, temperature and fuel feedback effects will
+coolant temperature $T_c$:
-change the total reactivity. Finally, control rods directly add or subtract
+%
-reactivity in the system by their movement. These equations were implemented in
+\begin{equation}
-a MATLAB code to simulate the simple reactor model. 
+  m_f c_{p,f} \frac{dT_f}{dt} = P(t) - h_{gap} A_s (T_f - T_c)
+  \label{eq:fuel_temp}
+\end{equation}
+%
+\begin{equation}
+  m_c c_{p,c} \frac{dT_c}{dt} = h_{gap} A_s (T_f - T_c)
+    - \dot{m} c_{p,c} (T_c - T_{inlet})
+  \label{eq:coolant_temp}
+\end{equation}
+%
+where $P(t)$ is the fission power proportional to $n(t)$, $h_{gap}$ is the
+gap heat transfer coefficient, $A_s$ is the heat transfer surface area,
+$\dot{m}$ is the coolant mass flow rate, and $T_{inlet}$ is the coolant
+inlet temperature.
+
+Reactivity is a sum of several different sources. First, reactivity is
+a factor of the fuel itself. Second, temperature feedback effects from both
+fuel and moderator will change the total reactivity. Finally, control rods
+directly add or subtract reactivity in the system by their movement:
+%
+\begin{equation}
+  \rho(t) = \rho_{ext}(t) + \alpha_f (T_f - T_{f,0})
+    + \alpha_m (T_c - T_{c,0})
+  \label{eq:reactivity}
+\end{equation}
+%
+where $\rho_{ext}$ is the externally applied reactivity from control rod
+position, $\alpha_f$ and $\alpha_m$ are the fuel and moderator temperature
+coefficients of reactivity, and $T_{f,0}$ and $T_{c,0}$ are reference
+temperatures. These equations were implemented in a MATLAB code to simulate
+the simple reactor model.
 
 First, a discrete controller was created by writing FRETish specifications
-according to diagram shown in figure \ref{fig:hybrid_automaton}. A full list of
+according to the diagram shown in Figure~\ref{fig:hybrid_automaton}. A full
-the specifications created is included in the \ref{APPENDIX}.\dasnote{need to
+list of the specifications created is included in
-actually create the appendix lmao}. This was then synthesized into an automaton
+Appendix~\ref{APPENDIX}.\dasnote{need to actually create the appendix}. This
-using (JKind? Kind2?)\dasnote{This will depend once reactive synthesis is done}.
+was then synthesized into an automaton using reactive synthesis
-Once this automaton was created, continuous controllers were developed in MATLAB
+tools.\dasnote{This will depend once reactive synthesis is done---JKind?
-for each discrete control mode. The end result was a hybrid system with discrete
+Kind2? Strix?} Once this automaton was created, continuous controllers were
-modes and continuous controllers created based on logical specifications, but
+developed in MATLAB for each discrete control mode. The end result was a
-were not yet verified. 
+hybrid system with discrete modes and continuous controllers created based
+on logical specifications, but were not yet verified.
 
 Once the continuous controllers were created, reachability analysis was
 performed on the transitory modes. For this example, there is only one
-transitory mode: the 'heatup' mode. For this mode, the entry temperature
+transitory mode: the heatup mode. For this mode, the entry temperature
-\(T_{MIN}\) was included as an entry condition, while other states were given
+$T_{MIN}$ was included as an entry condition, while other states were given
-physically reasonable bounds. Reachability analysis showed that the continuous
+physically reasonable bounds. Reachability analysis confirmed that the
-controller maintened the requirement as demonstrated in
+continuous controller satisfied the transitory mode requirement from
-\ref{eq:reachability}\dasnote{Need to make formal equations for earlier
+Section~3.2.1:\dasnote{Need to reference the specific reachability
-sections. That way we can reference them here easily}. 
+condition equation once earlier sections are finalized}
+%
+\[
+\text{Reach}(\mathcal{X}_{entry}, f_{heatup}, [0,T]) \subseteq
+\mathcal{X}_{safe} \land \text{Reach}(\mathcal{X}_{entry}, f_{heatup},
+[0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
+\]
 
 Once the transitory mode was complete, the stabilizing mode of power operation
-was analyzed using a barrier certificate search tool. % more needed here about
+was analyzed using a barrier certificate search.\dasnote{More needed here:
-%how this shit actually work. What are the bounds??
+what are the bounds of the invariant set? What tool was used for the SOS
+search? What degree polynomial for the barrier function?}
 
 Finally, the expulsory SCRAM mode was considered. For this example, the failure
 modes were kept relatively simple. We assumed possible failure modes of coolant
 fouling, where the coolant thermal properties have changed drastically, and a
 secondary system coolant leak, where power demand increases dramatically. For
 both of these cases, reachability analysis was performed to evaluate that the
-dynamics of the system could safely reach a low power low temperature state for
+dynamics of the system could safely reach a low power, low temperature state for
 the possible operating range of the reactor.
 
 \subsection{Industrial Implementation}