From 96af36972f97e013b5b4c2e336e6a07db6b1284d Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 16 Mar 2026 17:37:53 -0400 Subject: [PATCH] Fix all citations: add missing bib entries from Zotero, fix typos (lunz->lunze, katis_realizibility->realizability), add citations for hybrid automata (Alur), dL (Platzer), KeYmaera X (Fulton), barrier certificates (Prajna), reachability tools (Frehse SpaceEx, Guernic, Mitchell, Bansal HJ), Lyapunov (Branicky), convert biblatex->bibtex format --- 2-state-of-the-art/state-of-art.tex | 6 +- 3-research-approach/approach.tex | 31 ++- references.bib | 348 +++++++++++++++++++--------- 3 files changed, 259 insertions(+), 126 deletions(-) diff --git a/2-state-of-the-art/state-of-art.tex b/2-state-of-the-art/state-of-art.tex index 8b30e6a..744a608 100644 --- a/2-state-of-the-art/state-of-art.tex +++ b/2-state-of-the-art/state-of-art.tex @@ -187,7 +187,8 @@ existing documentation and verifiable system behavior. \subsubsection{Differential Dynamic Logic} A separate line of work extends temporal logics to verify hybrid systems -directly. The result has been the field of differential dynamic logic (dL). dL +directly. The result has been the field of differential dynamic logic +(dL)~\cite{platzer_differential_2008}. dL introduces two additional operators into temporal logic: the box operator and the diamond operator. The box operator \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system \(\alpha\) always remains within that @@ -200,7 +201,8 @@ liveness property. While dL allows for the specification of these liveness and safety properties, actually proving them for a given hybrid system is quite difficult. Automated -proof assistants such as KeYmaera X exist to help develop proofs of systems +proof assistants such as KeYmaera X~\cite{fulton_keymaera_2015} exist to help +develop proofs of systems using dL, but so far have been insufficient for reasonably complex hybrid systems. The main issue behind creating system proofs using dL is non-terminating solutions. Approaches have been made to alleviate these issues diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 72f17fd..661abbf 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -9,7 +9,7 @@ system. This means that the system does not have external input and that continuous states do not change instantaneously when discrete states change. For our systems of interest, the continuous states are physical quantities that are always Lipschitz continuous. This nomenclature is borrowed from the -Handbook on Hybrid Systems Control \cite{lunz_handbook_2009}, but is +Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is redefined here for convenience: \begin{equation} @@ -38,7 +38,8 @@ where: HAHACS bridges the gap between discrete and continuous verification by composing formal methods from computer science with control-theoretic verification, -formalizing reactor operations using the framework of hybrid automata. The +formalizing reactor operations using the framework of hybrid +automata~\cite{alur_hybrid_1993}. The challenge of hybrid system verification lies in the interaction between discrete and continuous dynamics. Discrete transitions change the active continuous vector field, creating discontinuities in the system's behavior. Traditional @@ -291,7 +292,7 @@ the current workforce becomes easier. A key feature of FRET is the ability to start with logically imprecise statements and consecutively refine them into well-posed -specifications\cite{katis_realizibility_2022, pressburger_using_2023}. We +specifications\cite{katis_realizability_2022, pressburger_using_2023}. We can use this to our advantage by directly importing operating procedures and design requirements into FRET in natural language, then iteratively refining them into specifications for a HAHACS. This has two distinct benefits. @@ -309,7 +310,8 @@ them to build the discrete control system. To do this, reactive synthesis tools are employed. Reactive synthesis is a field in computer science that deals with the automated creation of reactive programs from temporal logic specifications. A reactive program is one that, for a given state, takes an -input and produces an output\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the current +input and produces an output~\cite{jacobs_reactive_2024}. Our systems fit +exactly this mold: the current discrete state and status of guard conditions are the input, while the output is the next discrete state. @@ -339,7 +341,10 @@ controller using deterministic algorithms, discrete control decisions become provably consistent with operating procedures. (Talk about how one would go from a discrete automaton to actual -code)\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable +code)\splitsuggest{Consider citing Strix~\cite{meyer_strix_2018} as an +example reactive synthesis tool, even if you end up using a different one. +Also cite Katis conference version~\cite{katis_capture_2022} alongside the +report if you want both venues represented.}\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable LTL subset for synthesis: wins SYNTCOMP competitions (p.13). Luttenberger 2020 (Strix tool, pp.1-3) handles full LTL via parity games, achieving 4000+ state specs efficiently (p.5). Your nuclear procedures should fit @@ -444,7 +449,9 @@ exit condition without ever leaving the safe region. Verification of transitory modes will use reachability analysis. Reachability analysis computes the set of all states reachable from a given initial set -under the system dynamics\dasnote{cite reachability tools here}. For a transitory mode to be valid, the reachable +under the system dynamics~\cite{guernic_reachability_2009, +mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory +mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions: \begin{enumerate} \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the @@ -468,7 +475,8 @@ 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, and JuliaReach. The choice of tool depends on the +CORA, Flow*, SpaceEx~\cite{frehse_spaceex_2011}, and JuliaReach. 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 @@ -503,13 +511,14 @@ and load-following at constant power level. Reachability analysis for stabilizing modes may not be a suitable approach to validation. Instead, we plan to use barrier certificates. Barrier certificates analyze the dynamics of the system to determine whether flux across a given boundary -exists\dasnote{cite barrier certificate stuff here}. In other words, they +exists~\cite{prajna_safety_2004}. In other words, they evaluate whether any trajectory leaves a given boundary. This definition is exactly what defines the validity of a stabilizing continuous control mode. A barrier certificate (or control barrier function) is a scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a -safe set. The idea is analogous to Lyapunov functions for stability: rather +safe set. The idea is analogous to Lyapunov functions for +stability~\cite{branicky_multiple_1998}: rather than computing trajectories explicitly, we find a certificate function whose properties guarantee the desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, @@ -535,8 +544,8 @@ 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\dasnote{cite these -here}. The key +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 diff --git a/references.bib b/references.bib index b932bd6..e19ac60 100644 --- a/references.bib +++ b/references.bib @@ -10,7 +10,8 @@ title = {{10 CFR Part 50.34}}, author = {{U.S. Nuclear Regulatory Commission}}, howpublished = {Code of Federal Regulations}, - urldate = {2025-12-05}, + urlyear = {2025}, + month = dec, url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034} } @@ -18,50 +19,54 @@ title = {{10 CFR Part 55.59}}, author = {{U.S. Nuclear Regulatory Commission}}, howpublished = {Code of Federal Regulations}, - urldate = {2025-12-05}, + urlyear = {2025}, + month = dec, url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059} } -@techreport{WRPS.Description, - title = {{Westinghouse RPS System Description}}, - institution = {Westinghouse Electric Corporation}, - url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf}, - urldate = {2025-12-05} -} - -@online{gentillon_westinghouse_1999, - title = {Westinghouse Reactor Protection System Unavailability, 1984-1995}, - url = {https://digital.library.unt.edu/ark:/67531/metadc620476/}, - titleaddon = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999}, - type = {Article}, - author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.}, - urldate = {2025-12-05}, - date = {1999-08-01}, - note = {Number: {INEEL}/{CON}-99-00374 -Publisher: Idaho National Engineering and Environmental Laboratory}, - file = {Full Text PDF:/home/danesabo/Zotero/storage/7QKWQ8NI/Gentillon et al. - 1999 - Westinghouse Reactor Protection System Unavailability, 1984-1995.pdf:application/pdf}, -} - -@online{operator_statistics, - title = {{Operator Licensing}}, - author = {{U.S. Nuclear Regulatory Commission}}, - howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}}, - urldate = {2025-11-28}, - file = {Operator Licensing | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/KUP9B5GH/operator-licensing.html:text/html}, -} - @misc{10CFR55, title = {{Part 55—Operators' Licenses}}, author = {{U.S. Nuclear Regulatory Commission}}, howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}}, } -@online{10CFR50.54, +@misc{10CFR50.54, title = {{§ 50.54 Conditions of Licenses}}, author = {{U.S. Nuclear Regulatory Commission}}, howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}}, - urldate = {2025-11-28}, - file = {§ 50.54 Conditions of licenses. | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/THTZUD3T/part050-0054.html:text/html}, + urlyear = {2025}, + month = nov, +} + +@techreport{WRPS.Description, + author = {{Westinghouse Electric Corporation}}, + title = {{Westinghouse RPS System Description}}, + institution = {Westinghouse Electric Corporation}, + url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf}, + urlyear = {2025}, + month = dec +} + +@misc{gentillon_westinghouse_1999, + title = {Westinghouse Reactor Protection System Unavailability, 1984-1995}, + url = {https://digital.library.unt.edu/ark:/67531/metadc620476/}, + note = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999}, + type = {Article}, + author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.}, + urlyear = {2025}, + month = dec, + year = {1999}, + month = aug, + note = {Number: {INEEL}/{CON}-99-00374 +Publisher: Idaho National Engineering and Environmental Laboratory}, +} + +@misc{operator_statistics, + title = {{Operator Licensing}}, + author = {{U.S. Nuclear Regulatory Commission}}, + howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}}, + urlyear = {2025}, + month = nov, } @techreport{Kemeny1979, @@ -87,14 +92,14 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, doi = {10.1007/s13280-013-0382-x}, pages = {267--284}, number = {3}, - journaltitle = {Ambio}, - shortjournal = {Ambio}, + journal = {Ambio}, author = {Högberg, Lars}, - urldate = {2025-12-05}, - date = {2013-04}, + urlyear = {2025}, + month = dec, + year = {2013}, + month = apr, pmid = {23423737}, pmcid = {PMC3606704}, - file = {Full Text:/home/danesabo/Zotero/storage/E8F2QZGR/Högberg - 2013 - Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants.pdf:application/pdf}, } @article{zhang_analysis_2025, @@ -105,13 +110,13 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, doi = {10.1016/j.net.2025.103687}, pages = {103687}, number = {10}, - journaltitle = {Nuclear Engineering and Technology}, - shortjournal = {Nuclear Engineering and Technology}, + journal = {Nuclear Engineering and Technology}, author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng}, - urldate = {2025-12-05}, - date = {2025-10-01}, + urlyear = {2025}, + month = dec, + year = {2025}, + month = oct, keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports}, - file = {ScienceDirect Snapshot:/home/danesabo/Zotero/storage/N5R2Z3GL/S1738573325002554.html:text/html}, } @techreport{Kiniry2024, @@ -144,19 +149,92 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, } @book{baier_principles_2008, - location = {Cambridge, {MA}, {USA}}, + address = {Cambridge, {MA}, {USA}}, title = {Principles of Model Checking}, isbn = {978-0-262-02649-9}, abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.}, - pagetotal = {984}, publisher = {{MIT} Press}, author = {Baier, Christel and Katoen, Joost-Pieter}, - date = {2008-04-25}, - langid = {english}, + year = {2008}, + month = apr, +} + +@article{platzer_differential_2008, + title = {Differential {Dynamic} {Logic} for {Hybrid} {Systems}}, + volume = {41}, + issn = {1573-0670}, + url = {https://doi.org/10.1007/s10817-008-9103-8}, + doi = {10.1007/s10817-008-9103-8}, + abstract = {Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.}, + language = {en}, + number = {2}, + urlyear = {2025}, + month = sep, + journal = {Journal of Automated Reasoning}, + author = {Platzer, André}, + month = aug, + year = {2008}, + keywords = {Automated theorem proving, Axiomatisation, Differential equations, Dynamic logic, Sequent calculus, Verification of hybrid systems}, + pages = {143--189}, +} + +@inproceedings{fulton_keymaera_2015, + address = {Cham}, + title = {{KeYmaera} {X}: {An} {Axiomatic} {Tactical} {Theorem} {Prover} for {Hybrid} {Systems}}, + isbn = {978-3-319-21401-6}, + shorttitle = {{KeYmaera} {X}}, + doi = {10.1007/978-3-319-21401-6_36}, + abstract = {KeYmaera X is a theorem prover for differential dynamic logic (), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.}, + language = {en}, + booktitle = {Automated {Deduction} - {CADE}-25}, + publisher = {Springer International Publishing}, + author = {Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and Völp, Marcus and Platzer, André}, + editor = {Felty, Amy P. and Middeldorp, Aart}, + year = {2015}, + keywords = {Adaptive Cruise Control, Hybrid automaton, Proof Rule, Proof Tree, Sequent calculus}, + pages = {527--538}, +} + +@inproceedings{alur_hybrid_1993, + address = {Berlin, Heidelberg}, + title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}, + isbn = {978-3-540-48060-0}, + doi = {10.1007/3-540-57318-6_30}, + shorttitle = {Hybrid automata}, + pages = {209--229}, + booktitle = {Hybrid Systems}, + publisher = {Springer}, + author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin}, + editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans}, + year = {1993}, + keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem}, +} + +@techreport{katis_realizability_2022, + title = {Realizability {Checking} of {Requirements} in {FRET}}, + url = {https://ntrs.nasa.gov/citations/20220007510}, + abstract = {Requirements formalization has become increasingly popular in industrial settings as an +effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis +tools to prove important properties, such as consistency and realizability. In this report, +we present the realizability analysis framework that we developed as part of the Formal +Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs +state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of +conflicts between requirements and simulation of counterexamples, and discuss results from +industrial-level case studies.}, + urlyear = {2026}, + month = mar, + institution = {NASA Ames Research Center}, + author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann}, + month = apr, + year = {2022}, + note = {NTRS Author Affiliations: Wyle (United States), Ames Research Center +NTRS Document ID: 20220007510 +NTRS Research Center: Ames Research Center (ARC)}, + keywords = {Mathematical And Computer Sciences (General)}, } @inproceedings{katis_capture_2022, - location = {Cham}, + address = {Cham}, title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}}, isbn = {978-3-031-13188-2}, doi = {10.1007/978-3-031-13188-2_24}, @@ -166,13 +244,27 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, publisher = {Springer International Publishing}, author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann}, editor = {Shoham, Sharon and Vizel, Yakir}, - date = {2022}, - langid = {english}, - file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf}, + year = {2022}, +} + +@techreport{pressburger_using_2023, + title = {Using {FRET} to {Create}, {Analyze} and {Monitor} {Requirements} for a {Lift} {Plus} {Cruise} {Case} {Study}}, + url = {https://ntrs.nasa.gov/citations/20220017032}, + abstract = {In this technical report we provide information on the use of the NASA Formal RequirementsElicitation Tool (FRET) to create requirements for a Lift Plus Cruise (LPC) aircraft case study. Furthermore, we provide details on using FRET to translate these requirements into an appropriate format for the Copilot tool, enabling their usage to perform runtime verification on a synthesized LPC system.}, + urlyear = {2026}, + month = mar, + institution = {NASA Ames Research Center}, + author = {Pressburger, Thomas and Katis, Andreas and Dutle, Aaron and Mavridou, Anastasia}, + month = apr, + year = {2023}, + note = {NTRS Author Affiliations: Ames Research Center, KBR (United States), Langley Research Center +NTRS Document ID: 20220017032 +NTRS Research Center: Ames Research Center (ARC)}, + keywords = {Mathematical And Computer Sciences (General)}, } @inproceedings{meyer_strix_2018, - location = {Cham}, + address = {Cham}, title = {Strix: Explicit Reactive Synthesis Strikes Back!}, isbn = {978-3-319-96145-3}, doi = {10.1007/978-3-319-96145-3_31}, @@ -182,8 +274,7 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, publisher = {Springer International Publishing}, author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael}, editor = {Chockler, Hana and Weissenbacher, Georg}, - date = {2018}, - langid = {english}, + year = {2018}, } @misc{jacobs_reactive_2024, @@ -194,12 +285,26 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, number = {{arXiv}:2206.00251}, publisher = {{arXiv}}, author = {Jacobs, Swen and others}, - urldate = {2025-12-06}, - date = {2024-05-06}, - eprinttype = {arxiv}, - eprint = {2206.00251 [cs]}, + urlyear = {2025}, + month = dec, + year = {2024}, + month = may, keywords = {Computer Science - Logic in Computer Science}, - file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html}, +} + +@book{lunze_handbook_2009, + address = {Cambridge}, + title = {Handbook of {Hybrid} {Systems} {Control}: {Theory}, {Tools}, {Applications}}, + isbn = {978-0-521-76505-3}, + shorttitle = {Handbook of {Hybrid} {Systems} {Control}}, + url = {https://www.cambridge.org/core/books/handbook-of-hybrid-systems-control/95CBB51B339FA6B95B814D4BABB715A7}, + doi = {10.1017/CBO9780511807930}, + abstract = {Setting out core theory and reviewing a range of new methods, theoretical problems and applications, this handbook shows how hybrid dynamical systems can be modelled and understood. Sixty expert authors involved in the recent research activities and industrial application studies provide practical insights on topics ranging from the theoretical investigations over computer-aided design to applications in energy management and the process industry. Structured into three parts, the book opens with a thorough introduction to hybrid systems theory, illustrating new dynamical phenomena through numerous examples. Part II then provides a survey of key tools and tool integration activities. Finally, Part III is dedicated to applications, implementation issues and system integration, considering different domains such as industrial control, automotive systems and digital networks. Three running examples are referred to throughout the book, together with numerous illustrations, helping both researchers and industry professionals to understand complex theory, recognise problems and find appropriate solutions.}, + urlyear = {2026}, + month = jan, + publisher = {Cambridge University Press}, + editor = {Lunze, Jan and Lamnabhi-Lagarrigue, Françoise}, + year = {2009}, } @article{branicky_multiple_1998, @@ -210,41 +315,74 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, doi = {10.1109/9.664150}, pages = {475--482}, number = {4}, - journaltitle = {{IEEE} Transactions on Automatic Control}, + journal = {{IEEE} Transactions on Automatic Control}, author = {Branicky, M.S.}, - urldate = {2025-09-10}, - date = {1998-04}, + urlyear = {2025}, + month = sep, + year = {1998}, + month = apr, keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches}, - file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf}, } -@thesis{guernic_reachability_2009, +@phdthesis{kapuria_using_2025, + address = {United States -- Pennsylvania}, + type = {Ph.{D}.}, + title = {Using {Decomposition}-{Based} {Formal} {Verification} to {Analyze} {Safety} and {Identify} {Unsafe} {Control} {Actions} for {Hybrid} {Systems}}, + copyright = {Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.}, + isbn = {9798280700147}, + url = {https://www.proquest.com/docview/3215670525/abstract/3C715CB23CB84313PQ/1}, + abstract = {This dissertation presents a decomposition-based formal verification framework for hybrid systems, focusing on identifying unsafe control actions (UCAs) in cyber-physical systems (CPS). Using differential dynamic logic, we verify safety properties by first proving correctness at the component level before integrating them into a system-wide proof. Our approach enhances scalability by isolating subsystems, enforcing constraints on their interactions, and using satisfiability modulo theories (SMT) solvers to automate invariant generation. We apply this methodology to a small modular advanced high-temperature reactor (SmAHTR), analyzing its control logic under both normal operations and adversarial conditions, including cyberattacks. The results demonstrate how formal methods can systematically identify UCAs that emerge from mode transitions, feedback interactions, and incorrect assumptions. By integrating theorem proving with reachability analysis, this work advances CPS safety verification, providing a rigorous and scalable approach to ensuring system resilience. +To achieve this, we develop a hybrid automaton model of SmAHTR and formally verify its behavior under various control strategies, including scenarios involving maintenance operations and external disruptions. We introduce a structured method to decompose the system into independently analyzable components, ensuring that local safety guarantees extend to global system correctness. The verification process captures both intended and unintended control actions, revealing potential failure modes that traditional analysis methods might overlook. Furthermore, we propose an automated approach for identifying UCAs by leveraging formal reasoning tools to systematically explore system behaviors beyond manual hazard analysis. Our findings demonstrate that decomposition-based verification not only reduces computational complexity but also improves the efficiency and robustness of CPS safety analysis, particularly for high-assurance applications such as nuclear reactor operations.}, + language = {English}, + urlyear = {2026}, + month = feb, + school = {University of Pittsburgh}, + author = {Kapuria, Abhimanyu}, + year = {2025}, + keywords = {Computer science, Differential equations, Electrical engineering, Engineering, Formal verification, Hybrid systems, Mechanical engineering, Reachability analysis, Satisfiability modulo theories solvers}, +} + +@inproceedings{lang_formal_2021, + address = {VIRTUAL EVENT}, + title = {Formal {Verification} {Applied} to {Spacecraft} {Attitude} {Control}}, + isbn = {978-1-62410-609-5}, + url = {https://arc.aiaa.org/doi/10.2514/6.2021-1126}, + doi = {10.2514/6.2021-1126}, + language = {en}, + urlyear = {2024}, + month = nov, + booktitle = {{AIAA} {Scitech} 2021 {Forum}}, + publisher = {American Institute of Aeronautics and Astronautics}, + author = {Lang, Kendra and Klett, Corbin and Hawkins, Kelsey and Feron, Eric and Tsiotras, Panagiotis and Phillips, Sean}, + month = jan, + year = {2021}, +} + +@inproceedings{frehse_spaceex_2011, + address = {Berlin, Heidelberg}, + title = {{SpaceEx}: Scalable Verification of Hybrid Systems}, + isbn = {978-3-642-22110-1}, + doi = {10.1007/978-3-642-22110-1_30}, + shorttitle = {{SpaceEx}}, + pages = {379--395}, + booktitle = {Computer Aided Verification}, + publisher = {Springer}, + author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded}, + editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz}, + year = {2011}, + keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function}, +} + +@phdthesis{guernic_reachability_2009, title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics}, url = {https://theses.hal.science/tel-00422569}, institution = {Université Joseph-Fourier - Grenoble I}, - type = {phdthesis}, + school = {Université Joseph-Fourier, Grenoble}, author = {Guernic, Colas Le}, - urldate = {2025-09-14}, - date = {2009-10-28}, - langid = {english}, - file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf}, -} - -@inproceedings{alur_hybrid_1993, - location = {Berlin, Heidelberg}, - title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}, - isbn = {978-3-540-48060-0}, - doi = {10.1007/3-540-57318-6_30}, - shorttitle = {Hybrid automata}, - pages = {209--229}, - booktitle = {Hybrid Systems}, - publisher = {Springer}, - author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin}, - editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans}, - date = {1993}, - langid = {english}, - keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem}, - file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf}, + urlyear = {2025}, + month = sep, + year = {2009}, + month = oct, } @article{mitchell_time-dependent_2005, @@ -255,29 +393,13 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, doi = {10.1109/TAC.2005.851439}, pages = {947--957}, number = {7}, - journaltitle = {{IEEE} Transactions on Automatic Control}, + journal = {{IEEE} Transactions on Automatic Control}, author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.}, - urldate = {2025-09-15}, - date = {2005-07}, + urlyear = {2025}, + month = sep, + year = {2005}, + month = jul, keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity}, - file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf}, -} - -@inproceedings{frehse_spaceex_2011, - location = {Berlin, Heidelberg}, - title = {{SpaceEx}: Scalable Verification of Hybrid Systems}, - isbn = {978-3-642-22110-1}, - doi = {10.1007/978-3-642-22110-1_30}, - shorttitle = {{SpaceEx}}, - pages = {379--395}, - booktitle = {Computer Aided Verification}, - publisher = {Springer}, - author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded}, - editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz}, - date = {2011}, - langid = {english}, - keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function}, - file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf}, } @inproceedings{bansal_hamilton-jacobi_2017, @@ -289,14 +411,15 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, pages = {2242--2253}, booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.}, - urldate = {2025-09-15}, - date = {2017-12}, + urlyear = {2025}, + month = sep, + year = {2017}, + month = dec, keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials}, - file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf}, } @inproceedings{prajna_safety_2004, - location = {Berlin, Heidelberg}, + address = {Berlin, Heidelberg}, title = {Safety Verification of Hybrid Systems Using Barrier Certificates}, isbn = {978-3-540-24743-2}, doi = {10.1007/978-3-540-24743-2_32}, @@ -305,7 +428,6 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, publisher = {Springer}, author = {Prajna, Stephen and Jadbabaie, Ali}, editor = {Alur, Rajeev and Pappas, George J.}, - date = {2004}, - langid = {english}, + year = {2004}, keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis}, }