Checked ALL references. V1 is COMPLETE!
This commit is contained in:
Dane Sabo
parent
9c5289705c
commit
1ba14bc8d7
@ -67,14 +67,13 @@ flexibility and safety assurance remains unresolved: the person responsible for
|
||||
reactor safety is often the root cause of failures.
|
||||
|
||||
Multiple independent analyses converge on a striking statistic: 70--80\% of
|
||||
nuclear power plant events are attributed to human error, versus
|
||||
approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
|
||||
the root cause of all severe accidents at nuclear power plants---Three Mile
|
||||
Island, Chernobyl, and Fukushima Daiichi---has been identified as primarily human
|
||||
factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
|
||||
Chinese nuclear power plants from
|
||||
2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
|
||||
active errors, while 92\% were associated with latent
|
||||
nuclear power plant events are attributed to human error, versus approximately
|
||||
20\% to equipment failures~\cite{noauthor_human_nodate}. More significantly, the
|
||||
root cause of all severe accidents at nuclear power plants---Three Mile Island,
|
||||
Chernobyl, and Fukushima Daiichi---has been identified as primarily human
|
||||
factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at Chinese
|
||||
nuclear power plants from 2007--2020~\cite{zhang_analysis_2025} found that 53\%
|
||||
of events involved active errors, while 92\% were associated with latent
|
||||
errors---organizational and systemic weaknesses that create conditions for
|
||||
failure.
|
||||
|
||||
@ -99,20 +98,18 @@ regulatory criteria. The project delivered a Reactor Trip System (RTS)
|
||||
implementation with traceability from regulatory requirements to verified
|
||||
software through formal architecture specifications.
|
||||
|
||||
HARDENS employed formal methods tools at
|
||||
every level of system development, from high-level requirements through
|
||||
executable models to generated code. High-level specifications used
|
||||
Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
|
||||
capture stakeholder requirements, domain engineering, certification
|
||||
requirements, and safety requirements. Requirements were analyzed for
|
||||
consistency, completeness, and realizability using SAT and SMT solvers.
|
||||
Executable formal models used Cryptol to create a behavioral model of the
|
||||
entire RTS, including all subsystems, components, and limited digital twin
|
||||
models of sensors, actuators, and compute infrastructure. Automatic code
|
||||
synthesis generated verifiable C implementations and SystemVerilog hardware
|
||||
implementations directly from Cryptol models---eliminating the traditional
|
||||
gap between specification and implementation where errors commonly
|
||||
arise.
|
||||
HARDENS employed formal methods tools at every level of system development, from
|
||||
high-level requirements through executable models to generated code. High-level
|
||||
specifications used Lando, SysMLv2, and FRET (NASA Formal Requirements
|
||||
Elicitation Tool) to capture stakeholder requirements, domain engineering,
|
||||
certification requirements, and safety requirements. Requirements were analyzed
|
||||
for consistency, completeness, and realizability using SAT and SMT solvers.
|
||||
Executable formal models used Cryptol to create a behavioral model of the entire
|
||||
RTS, including all subsystems, components, and limited digital twin models of
|
||||
sensors, actuators, and compute infrastructure. Automatic code synthesis
|
||||
generated verifiable C implementations and SystemVerilog hardware
|
||||
implementations directly from Cryptol models---eliminating the traditional gap
|
||||
between specification and implementation where errors commonly arise.
|
||||
|
||||
Despite these accomplishments, HARDENS addressed only discrete digital
|
||||
control logic. The Reactor Trip System verification covered discrete state
|
||||
|
||||
@ -136,18 +136,19 @@ behavior within each mode.
|
||||
\subsection{System Requirements, Specifications, and Discrete Controllers}
|
||||
|
||||
Human control of nuclear power can be divided into three different scopes:
|
||||
strategic, operational, and tactical. Strategic control is 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 scheduled maintenance and downtime. The time scale at this level is
|
||||
long, often spanning months or years. The lowest level of control is the
|
||||
tactical level. This is the individual control of pumps, turbines, and
|
||||
chemistry. Tactical control has already been somewhat automated in nuclear power
|
||||
plants today, and is generally considered ``automatic control'' when autonomous.
|
||||
These controls are almost always continuous systems with a direct impact on the
|
||||
physical state of the plant. Tactical control objectives include, but are not
|
||||
limited to, maintaining pressurizer level, maintaining core temperature, or
|
||||
adjusting reactivity with a chemical shim.
|
||||
strategic, operational, and tactical.\footnote{This was inspired by an article
|
||||
about battlefield organizational science~\cite{harvey_levels_2021}.} Strategic
|
||||
control is 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 scheduled maintenance and downtime. The time
|
||||
scale at this level is long, often spanning months or years. The lowest level of
|
||||
control is the tactical level. This is the individual control of pumps,
|
||||
turbines, and chemistry. Tactical control has already been somewhat automated in
|
||||
nuclear power plants today, and is generally considered ``automatic control''
|
||||
when autonomous. These controls are almost always continuous systems with a
|
||||
direct impact on the physical state of the plant. Tactical control objectives
|
||||
include, but are not limited to, maintaining pressurizer level, maintaining core
|
||||
temperature, or adjusting reactivity with a chemical shim.
|
||||
|
||||
The level of control linking these two extremes is the operational control
|
||||
scope. Operational control is the primary responsibility of human operators
|
||||
@ -157,8 +158,8 @@ way, it bridges high-level and low-level goals. A strategic goal may be to
|
||||
perform refueling at a certain time, while the tactical level of the plant is
|
||||
currently focused on maintaining a certain core temperature. The operational
|
||||
level issues the shutdown procedure, using several smaller tactical goals along
|
||||
the way to achieve this strategic objective. This heiarchal division of control
|
||||
scope and objectives is illustrated graphically in
|
||||
the way to achieve this strategic objective. This hierarchical division of
|
||||
control scope and objectives is illustrated graphically in
|
||||
figure~\ref{fig:strat_op_tact}.
|
||||
|
||||
\begin{figure}
|
||||
@ -331,17 +332,17 @@ controller using deterministic algorithms, discrete control decisions become
|
||||
provably consistent with operating procedures.
|
||||
|
||||
The output of reactive synthesis is a finite-state machine that can be directly
|
||||
translated to executable code. Tools such as Strix~\cite{meyer_strix_2018}
|
||||
accept full LTL specifications and produce Mealy machines via parity game
|
||||
solving~\cite{katis_capture_2022}. For specifications within the GR(1)
|
||||
fragment---which captures the reactive input-output structure typical of
|
||||
supervisory control---synthesis is efficient and scales to specifications with
|
||||
thousands of states. Nuclear operating procedures are well-suited to this
|
||||
fragment: environment inputs correspond to plant state measurements and guard
|
||||
conditions, while outputs are mode transition commands. The synthesized
|
||||
automaton provides a correct-by-construction implementation that can be compiled
|
||||
to run on industrial control hardware without manual translation of the control
|
||||
logic.
|
||||
translated to executable code. Tools such as Strix accept full LTL
|
||||
specifications and produce Mealy machines via parity game
|
||||
solving~\cite{luttenberger_practical_2020, meyer_strix_2018}. For specifications
|
||||
within the GR(1) fragment---which captures the reactive input-output structure
|
||||
typical of supervisory control---synthesis is efficient and scales to
|
||||
specifications with thousands of states. Nuclear operating procedures are
|
||||
well-suited to this fragment: environment inputs correspond to plant state
|
||||
measurements and guard conditions, while outputs are mode transition commands.
|
||||
The synthesized automaton provides a correct-by-construction implementation that
|
||||
can be compiled to run on industrial control hardware without manual translation
|
||||
of the control logic.
|
||||
|
||||
\subsection{Continuous Control Modes}
|
||||
|
||||
@ -362,13 +363,12 @@ discrete layer to produce a safe hybrid system.
|
||||
|
||||
The operational control scope defines go/no-go decisions that determine what
|
||||
kind of continuous control to implement. The entry or exit conditions of a
|
||||
discrete state are themselves the guard conditions $\mathcal{G}$ that define
|
||||
the boundaries for each continuous controller's allowed state-space region.
|
||||
These continuous controllers all share a common state space, but each
|
||||
individual continuous control mode operates within its own partition defined
|
||||
by the discrete state $q_i$ and the associated guard conditions.
|
||||
This partitioning of the continuous state space among several
|
||||
distinct vector fields has
|
||||
discrete state are themselves the guard conditions $\mathcal{G}$ that define the
|
||||
boundaries for each continuous controller's allowed state-space region. These
|
||||
continuous controllers all share a common state space, but each individual
|
||||
continuous control mode operates within its own partition defined by the
|
||||
discrete state $q_i$ and the associated guard conditions. This partitioning of
|
||||
the continuous state space among several distinct vector fields has
|
||||
traditionally been a difficult problem for validation and verification. The
|
||||
discontinuity of the vector fields at discrete state interfaces makes
|
||||
reachability analysis computationally expensive, and analytic solutions often
|
||||
@ -458,7 +458,9 @@ confirm that the candidate continuous controller achieves the objective from
|
||||
all possible starting points.
|
||||
|
||||
Several tools exist for computing reachable sets of hybrid systems, including
|
||||
CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. The choice of
|
||||
CORA~\cite{althoff_introduction_nodate}, Flow*~\cite{chen_flow_2013,
|
||||
chen_taylor_2012}, SpaceEx~\cite{frehse_spaceex_2011}, and
|
||||
JuliaReach~\cite{bogomolov_reachability_2020}. The choice of
|
||||
tool depends on the structure of the continuous dynamics. Linear systems admit
|
||||
efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems
|
||||
require more conservative over-approximations using techniques such as Taylor
|
||||
@ -507,26 +509,23 @@ and minimizes complication in validating stabilizing continuous control modes.
|
||||
The discrete specifications tell us what region must be invariant; the barrier
|
||||
certificate confirms that the candidate controller achieves this invariance.
|
||||
|
||||
Finding barrier certificates can be formulated as a sum-of-squares (SOS)
|
||||
optimization problem for polynomial systems, or solved using satisfiability
|
||||
modulo theories (SMT) solvers for broader classes of
|
||||
dynamics~\cite{prajna_safety_2004, kapuria_using_2025}. The key advantage is
|
||||
that the verification is independent of how the controller was designed.
|
||||
Standard control techniques can be used to build continuous controllers, and
|
||||
barrier certificates provide a separate check that the result satisfies the
|
||||
required invariants. This also allows for the checking of control modes with
|
||||
different models than they are designed for. For example, a lower fidelity model
|
||||
can be used for controller design, but a higher fidelity model can be used for
|
||||
the actual validation of that stabilizing controller.\splitnote{SOS methods
|
||||
proven effective: Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier
|
||||
certificate optimization via SOS constraints---tool integrates with MATLAB.
|
||||
Borrmann 2015 (pp.4-8) demonstrates control barrier certificates for
|
||||
multi-agent systems, showing how discrete boundaries (mode guards) can inform
|
||||
barrier design. Your claim that discrete specs eliminate barrier search is
|
||||
novel and well-supported by these foundations.}\splitnote{Hauswirth 2024
|
||||
(pp.1-3) shows optimization-based robust feedback controllers can serve as
|
||||
alternative verification method---suggests barrier certificates + reachability
|
||||
provide complementary guarantees for your stabilizing modes.}
|
||||
The key advantage is that the verification is independent of how the controller
|
||||
was designed. Standard control techniques can be used to build continuous
|
||||
controllers, and barrier certificates provide a separate check that the result
|
||||
satisfies the required invariants. This also allows for the checking of control
|
||||
modes with different models than they are designed for. For example, a lower
|
||||
fidelity model can be used for controller design, but a higher fidelity model
|
||||
can be used for the actual validation of that stabilizing
|
||||
controller.\splitnote{SOS methods proven effective: Papachristodoulou 2021
|
||||
(SOSTOOLS v4, pp.1-2) solves barrier certificate optimization via SOS
|
||||
constraints---tool integrates with MATLAB. Borrmann 2015 (pp.4-8) demonstrates
|
||||
control barrier certificates for multi-agent systems, showing how discrete
|
||||
boundaries (mode guards) can inform barrier design. Your claim that discrete
|
||||
specs eliminate barrier search is novel and well-supported by these
|
||||
foundations.}\splitnote{Hauswirth 2024 (pp.1-3) shows optimization-based robust
|
||||
feedback controllers can serve as alternative verification method---suggests
|
||||
barrier certificates + reachability provide complementary guarantees for your
|
||||
stabilizing modes.}
|
||||
|
||||
\subsubsection{Expulsory Modes}
|
||||
|
||||
|
||||
102
references.bib
102
references.bib
@ -77,6 +77,12 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
|
||||
month = {October}
|
||||
}
|
||||
|
||||
@article{noauthor_human_nodate,
|
||||
title = {Human {Performance} {Improvement} {Handbook}, {Volume} 1},
|
||||
language = {en},
|
||||
file = {PDF:/Users/danesabo/Zotero/storage/HQZTH3YI/Human Performance Improvement Handbook, Volume 1.pdf:application/pdf},
|
||||
}
|
||||
|
||||
@misc{WNA2020,
|
||||
title = {Safety of Nuclear Power Reactors},
|
||||
author = {{World Nuclear Association}},
|
||||
@ -440,3 +446,99 @@ To achieve this, we develop a hybrid automaton model of SmAHTR and formally veri
|
||||
type = {Ifri Papers},
|
||||
isbn = {979-10-373-1000-2}
|
||||
}
|
||||
|
||||
|
||||
@article{harvey_levels_2021,
|
||||
title = {The {Levels} of {War} as {Levels} of {Analysis}},
|
||||
language = {en},
|
||||
publisher = {Military Review},
|
||||
author = {Harvey, Andrew S},
|
||||
year = {2021},
|
||||
file = {PDF:/Users/danesabo/Zotero/storage/5NSKMNEU/Harvey - The Levels of War as Levels of Analysis.pdf:application/pdf},
|
||||
}
|
||||
|
||||
@article{luttenberger_practical_2020,
|
||||
title = {Practical synthesis of reactive systems from {LTL} specifications via parity games},
|
||||
volume = {57},
|
||||
issn = {1432-0525},
|
||||
url = {https://doi.org/10.1007/s00236-019-00349-3},
|
||||
doi = {10.1007/s00236-019-00349-3},
|
||||
abstract = {The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.},
|
||||
language = {en},
|
||||
number = {1},
|
||||
urldate = {2026-03-07},
|
||||
journal = {Acta Informatica},
|
||||
author = {Luttenberger, Michael and Meyer, Philipp J. and Sickert, Salomon},
|
||||
month = apr,
|
||||
year = {2020},
|
||||
pages = {3--36},
|
||||
file = {Submitted Version:/Users/danesabo/Zotero/storage/VYMVF5GK/Luttenberger et al. - 2020 - Practical synthesis of reactive systems from LTL specifications via parity games.pdf:application/pdf},
|
||||
}
|
||||
|
||||
|
||||
@inproceedings{chen_taylor_2012,
|
||||
title = {Taylor {Model} {Flowpipe} {Construction} for {Non}-linear {Hybrid} {Systems}},
|
||||
issn = {1052-8725},
|
||||
url = {https://ieeexplore.ieee.org/document/6424802},
|
||||
doi = {10.1109/RTSS.2012.70},
|
||||
abstract = {We propose an approach for verifying non-linear hybrid systems using higher-order Taylor models that are a combination of bounded degree polynomials over the initial conditions and time, bloated by an interval. Taylor models are an effective means for computing rigorous bounds on the complex time trajectories of non-linear differential equations. As a result, Taylor models have been successfully used to verify properties of non-linear continuous systems. However, the handling of discrete (controller) transitions remains a challenging problem. In this paper, we provide techniques for handling the effect of discrete transitions on Taylor model flow pipe construction. We explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We provide an implementation of the techniques described in the paper and evaluate the various design choices over a set of challenging benchmarks.},
|
||||
urldate = {2026-03-18},
|
||||
booktitle = {2012 {IEEE} 33rd {Real}-{Time} {Systems} {Symposium}},
|
||||
author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
|
||||
month = dec,
|
||||
year = {2012},
|
||||
note = {ISSN: 1052-8725},
|
||||
keywords = {Approximation methods, Computational modeling, Mathematical model, Polynomials, Safety, Taylor series, Trajectory},
|
||||
pages = {183--192},
|
||||
file = {Snapshot:/Users/danesabo/Zotero/storage/7HBF3VMT/6424802.html:text/html},
|
||||
}
|
||||
|
||||
@inproceedings{chen_flow_2013,
|
||||
address = {Berlin, Heidelberg},
|
||||
title = {Flow*: {An} {Analyzer} for {Non}-linear {Hybrid} {Systems}},
|
||||
isbn = {978-3-642-39799-8},
|
||||
shorttitle = {Flow*},
|
||||
doi = {10.1007/978-3-642-39799-8_18},
|
||||
abstract = {The tool Flow* performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. Flow* combines well-known Taylor model arithmetic techniques for guaranteed approximations of the continuous dynamics in each mode with a combination of approaches for handling mode invariants and discrete transitions. Flow* supports a wide variety of optimizations including adaptive step sizes, adaptive selection of approximation orders and the heuristic selection of template directions for aggregating flowpipes. This paper describes Flow* and demonstrates its performance on a series of non-linear continuous and hybrid system benchmarks. Our comparisons show that Flow* is competitive with other tools.},
|
||||
language = {en},
|
||||
booktitle = {Computer {Aided} {Verification}},
|
||||
publisher = {Springer},
|
||||
author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
|
||||
editor = {Sharygina, Natasha and Veith, Helmut},
|
||||
year = {2013},
|
||||
keywords = {Adaptive Step, Adaptive Step Size, Discrete Transition, Hybrid System, Taylor Model},
|
||||
pages = {258--263},
|
||||
file = {Full Text PDF:/Users/danesabo/Zotero/storage/6QV2XCVF/Chen et al. - 2013 - Flow An Analyzer for Non-linear Hybrid Systems.pdf:application/pdf},
|
||||
}
|
||||
|
||||
|
||||
@inproceedings{althoff_introduction_nodate,
|
||||
title = {An {Introduction} to {CORA} 2015},
|
||||
url = {https://easychair.org/publications/paper/xMm},
|
||||
doi = {10.29007/zbkv},
|
||||
abstract = {The philosophy, architecture, and capabilities of the COntinuous Reachability Analyzer (CORA) are presented. CORA is a toolbox that integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis. CORA has a modular design, making it possible to use the capabilities of the various set representations for other purposes besides reachability analysis. The toolbox is designed using the object oriented paradigm, such that users can safely use methods without concerning themselves with detailed information hidden inside the object. Since the toolbox is written in MATLAB, the installation and use is platform independent.},
|
||||
urldate = {2026-03-18},
|
||||
author = {Althoff, Matthias},
|
||||
pages = {120--87},
|
||||
file = {Full Text:/Users/danesabo/Zotero/storage/BIGJMRCV/Althoff - An Introduction to CORA 2015.pdf:application/pdf},
|
||||
}
|
||||
|
||||
|
||||
@article{bogomolov_reachability_2020,
|
||||
title = {Reachability {Analysis} of {Linear} {Hybrid} {Systems} via {Block} {Decomposition}},
|
||||
volume = {39},
|
||||
issn = {1937-4151},
|
||||
url = {https://ieeexplore.ieee.org/document/9211556},
|
||||
doi = {10.1109/TCAD.2020.3012859},
|
||||
abstract = {Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.},
|
||||
number = {11},
|
||||
urldate = {2026-03-18},
|
||||
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
|
||||
author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
|
||||
month = nov,
|
||||
year = {2020},
|
||||
keywords = {Approximation algorithms, Decomposition, Design automation, Heuristic algorithms, hybrid systems, Integrated circuits, Linear systems, reachability, Reachability analysis, Tools},
|
||||
pages = {4018--4029},
|
||||
file = {Snapshot:/Users/danesabo/Zotero/storage/D7FYXW7T/9211556.html:text/html;Submitted Version:/Users/danesabo/Zotero/storage/I3HNBQ65/Bogomolov et al. - 2020 - Reachability Analysis of Linear Hybrid Systems via Block Decomposition.pdf:application/pdf},
|
||||
}
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user