vault backup: 2024-10-16 09:45:08

2024-10-16 09:45:09 -04:00 · 2024-10-16 09:45:09 -04:00 · 42b7d8ab75
commit 42b7d8ab75
parent 1d4018aafe
3 changed files with 34 additions and 4 deletions
--- a/.obsidian/plugins/obsidian-pandoc-reference-list/data.json
+++ b/.obsidian/plugins/obsidian-pandoc-reference-list/data.json
@ -1,8 +1,16 @@
 {
  "pathToPandoc": "/app/bin/pandoc",
  "tooltipDelay": 400,
-  "zoteroGroups": [],
+  "zoteroGroups": [
+    {
+      "id": 1,
+      "name": "My Library",
+      "lastUpdate": 1729086294988
+    }
+  ],
  "renderCitations": true,
  "renderCitationsReadingMode": true,
-  "renderLinkCitations": true
+  "renderLinkCitations": true,
+  "pullFromZotero": true,
+  "cslStyleURL": "https://raw.githubusercontent.com/citation-style-language/styles/master/ieee.csl"
 }
--- a/.pandoc/zotero-library-1.json
+++ b/.pandoc/zotero-library-1.json
@ -53,6 +53,7 @@
  {"id":"askarpourFormalMethodsDesigning2019","accessed":{"date-parts":[["2023",11,3]]},"author":[{"family":"Askarpour","given":"Mehrnoosh"},{"family":"Ghezzi","given":"Carlo"},{"family":"Mandrioli","given":"Dino"},{"family":"Rossi","given":"Matteo"},{"family":"Tsigkanos","given":"Christos"}],"citation-key":"askarpourFormalMethodsDesigning2019","container-title":"From Software Engineering to Formal Methods and Tools, and Back","DOI":"10.1007/978-3-030-30985-5_8","editor":[{"family":"Ter Beek","given":"Maurice H."},{"family":"Fantechi","given":"Alessandro"},{"family":"Semini","given":"Laura"}],"event-place":"Cham","ISBN":"978-3-030-30984-8 978-3-030-30985-5","issued":{"date-parts":[["2019"]]},"language":"en","page":"110-130","publisher":"Springer International Publishing","publisher-place":"Cham","source":"DOI.org (Crossref)","title":"Formal Methods in Designing Critical Cyber-Physical Systems","type":"chapter","URL":"http://link.springer.com/10.1007/978-3-030-30985-5_8","volume":"11865"},
  {"id":"askarpourFormalMethodsDesigning2019a","abstract":"Cyber-Physical Systems (CPS) are increasingly applied in critical contexts, where they have to support safe and secure operations, often subject to stringent timing requirements. Typical examples are scenarios involving automated living or working spaces in which humans operate, or human-robot collaborations (HRC) in modern manufacturing. Formal methods have been traditionally investigated to support modeling and veriﬁcation of critical systems. In this paper, we review some of the main new challenges arising in the application of formal methods to modeling and veriﬁcation of CPS. We do that by presenting two case studies (emergency response in a smart city and a smart manufacturing system), reﬂecting past work of the authors, from which some general lessons are distilled.","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Askarpour","given":"Mehrnoosh"},{"family":"Ghezzi","given":"Carlo"},{"family":"Mandrioli","given":"Dino"},{"family":"Rossi","given":"Matteo"},{"family":"Tsigkanos","given":"Christos"}],"citation-key":"askarpourFormalMethodsDesigning2019a","container-title":"From Software Engineering to Formal Methods and Tools, and Back","DOI":"10.1007/978-3-030-30985-5_8","editor":[{"family":"Ter Beek","given":"Maurice H."},{"family":"Fantechi","given":"Alessandro"},{"family":"Semini","given":"Laura"}],"event-place":"Cham","ISBN":"978-3-030-30984-8 978-3-030-30985-5","issued":{"date-parts":[["2019"]]},"language":"en","page":"110-130","publisher":"Springer International Publishing","publisher-place":"Cham","source":"DOI.org (Crossref)","title":"Formal Methods in Designing Critical Cyber-Physical Systems","type":"chapter","URL":"http://link.springer.com/10.1007/978-3-030-30985-5_8","volume":"11865"},
  {"id":"askarpourFormalModelHuman2019","abstract":"Recent developments in manufacturing technologies, also known as Industry 4.0, seek to build Smart Factories where supply chains and production lines are equipped with a higher level of automation. However, this significant innovation does not entirely eliminate the need for the presence of human operators; on the contrary, it requires them to collaborate with robots and execute hybrid tasks. Thus, creating safe workspaces for human operators is crucial for the future of factories where humans and robots collaborate closely in common workspaces. The uncertainty of human behavior and, consequently, of the actual execution of workflows, pose significant challenges to the safety of collaborative applications. This paper extends our earlier work, a formal verification methodology to analyze the safety of collaborative robotics applications (Askarpour et al. 2017) [1], with a rich non-deterministic formal model of operator behaviors that captures the hazardous situations resulting from human errors. The model allows safety engineers to refine their designs until all plausible erroneous behaviors are considered and mitigated. The solidity of the proposed approach is evaluated on a pair of real-life case studies.","accessed":{"date-parts":[["2023",10,13]]},"author":[{"family":"Askarpour","given":"Mehrnoosh"},{"family":"Mandrioli","given":"Dino"},{"family":"Rossi","given":"Matteo"},{"family":"Vicentini","given":"Federico"}],"citation-key":"askarpourFormalModelHuman2019","container-title":"Robotics and Computer-Integrated Manufacturing","container-title-short":"Robotics and Computer-Integrated Manufacturing","DOI":"10.1016/j.rcim.2019.01.001","ISSN":"07365845","issued":{"date-parts":[["2019",6]]},"language":"en","page":"465-476","source":"DOI.org (Crossref)","title":"Formal model of human erroneous behavior for safety analysis in collaborative robotics","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S0736584518303247","volume":"57"},
+  {"id":"atsumiModifiedBodePlots2012","abstract":"We have developed a loop-shaping methodology for robust control design in single-input single-output (SISO) systems with structured and unstructured uncertainties. This design method employs visualization tools that are modifications of the classical Bode plot. Using the proposed method control engineers can easily consider the effects of the structured and unstructured uncertainties without the need for transfer-function models of the plant, the sensitivity function performance, or the uncertainty. The method simultaneously can avoid excessive conservativeness and excessively high order controllers while improving controller performance and robustness. We show utility of the proposed method by applying it to a head-positioning control system in a hard disk drive.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Atsumi","given":"Takenori"},{"family":"Messner","given":"William C."}],"citation-key":"atsumiModifiedBodePlots2012","container-title":"IEEE Transactions on Control Systems Technology","DOI":"10.1109/TCST.2011.2177978","ISSN":"1558-0865","issue":"2","issued":{"date-parts":[["2012",3]]},"page":"356-368","source":"IEEE Xplore","title":"Modified Bode Plots for Robust Performance in SISO Systems With Structured and Unstructured Uncertainties","type":"article-journal","URL":"https://ieeexplore.ieee.org/abstract/document/6119239?casa_token=83yuiE-hjFYAAAAA:mNJC01cIlFnpVQ9rlmT3ddenFytwYuhZvrofSUb5nUDlMuEhcqDo8ZNGdmZHpey3BVXdGAfgig","volume":"20"},
  {"id":"avigadFORMALSYSTEMEUCLID2009","abstract":"We present a formal system, E, which provides a faithful model of the proofs in Euclid’s Elements, including the use of diagrammatic reasoning.","accessed":{"date-parts":[["2024",5,16]]},"author":[{"family":"Avigad","given":"Jeremy"},{"family":"Dean","given":"Edward"},{"family":"Mumma","given":"John"}],"citation-key":"avigadFORMALSYSTEMEUCLID2009","container-title":"The Review of Symbolic Logic","container-title-short":"The Review of Symbolic Logic","DOI":"10.1017/S1755020309990098","ISSN":"1755-0203, 1755-0211","issue":"4","issued":{"date-parts":[["2009",12]]},"language":"en","license":"https://www.cambridge.org/core/terms","page":"700-768","source":"DOI.org (Crossref)","title":"A FORMAL SYSTEM FOR EUCLID’S <i>ELEMENTS</i>","type":"article-journal","URL":"https://www.cambridge.org/core/product/identifier/S1755020309990098/type/journal_article","volume":"2"},
  {"id":"AWS","citation-key":"AWS","issued":{"literal":"date accessed 03/24/2022"},"title":"AWS IoT Twin Maker","type":"webpage","URL":"https://aws.amazon.com/iot-twinmaker/"},
  {"id":"ayo-imoruEnhancedFaultDiagnosis2021","abstract":"Nuclear power plants can provide a huge amount of clean energy, which can help most countries to meet their greenhouse gas emission requirements according to the Paris agreement on climate change. To meet this energy need, the nuclear plant must be operated safely and economically, which makes the digital twin concept viable for achieving this aim. The digital twin can be used to monitor plant condition, fault diagnosis, prediction, and plant maintenance support systems. In this work, the framework for digital twin in a nuclear plant is proposed. This framework combines the application of the nuclear plant simulator and machine learning tools. The machine learning aspect of this digital twin concept is the focus of this paper. Data was generated by using a personal computer-based nuclear plant simulator. Principal component analysis was used in reducing the data dimension. Artificial neural networks and adaptive neuro-fuzzy inference systems were trained with the reduced data and used to diagnose the faults. Four faults in the plant were diagnosed with minimal error. The fault diagnosis is a significant aspect of the digital twin framework.","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Ayo-Imoru","given":"Ronke M."},{"family":"Ali","given":"Ahmed A."},{"family":"Bokoro","given":"Pitshou N."}],"citation-key":"ayo-imoruEnhancedFaultDiagnosis2021","container-title":"2021 International Conference on Electrical, Computer and Energy Technologies (ICECET)","DOI":"10.1109/ICECET52533.2021.9698715","event-place":"Cape Town, South Africa","event-title":"2021 International Conference on Electrical, Computer and Energy Technologies (ICECET)","ISBN":"978-1-66544-231-2","issued":{"date-parts":[["2021",12,9]]},"language":"en","page":"1-6","publisher":"IEEE","publisher-place":"Cape Town, South Africa","source":"DOI.org (Crossref)","title":"An enhanced fault diagnosis in nuclear power plants for a digital twin framework","type":"paper-conference","URL":"https://ieeexplore.ieee.org/document/9698715/"},
@ -120,9 +121,10 @@
  {"id":"brockApplicationReinforcementLearning2021","abstract":"With the proliferation of advanced metering infrastructure (AMI), more real-time data is available to electric utilities and consumers. Such high volumes of data facilitate innovative electricity rate structures beyond flat-rate and time-of-use (TOU) tariffs. One such innovation is real-time pricing (RTP), in which the wholesale market-clearing price is passed directly to the consumer on an hour-by-hour basis. While rare, RTP exists in parts of the United States and has been observed to reduce electric bills. Although these reductions are largely incidental, RTP may represent an opportunity for large-scale peak shaving, demand response, and economic efficiency when paired with intelligent control systems. Algorithms controlling flexible loads and energy storage have been deployed for demand response elsewhere in the literature, but few studies have investigated these algorithms in an RTP environment. If properly optimized, the dynamic between RTP and intelligent control has the potential to counteract the unwelcome spikes and dips of demand driven by growing penetration of distributed renewable generation and electric vehicles (EV). This paper presents a simple reinforcement learning (RL) application for optimal battery control subject to an RTP signal.","accessed":{"date-parts":[["2022",3,25]]},"author":[{"family":"Brock","given":"Eli"},{"family":"Bruckstein","given":"Lauren"},{"family":"Connor","given":"Patrick"},{"family":"Nguyen","given":"Sabrina"},{"family":"Kerestes","given":"Robert"},{"family":"Abdelhakim","given":"Mai"}],"citation-key":"brockApplicationReinforcementLearning2021","container-title":"arXiv:2111.11367 [cs, eess]","issued":{"date-parts":[["2021",11,22]]},"source":"arXiv.org","title":"An application of reinforcement learning to residential energy storage under real-time pricing","type":"article-journal","URL":"http://arxiv.org/abs/2111.11367"},
  {"id":"brosinskyEmbeddedDigitalTwins2020","abstract":"Emerging real-time applications in information technology, and operational technology enable new innovative concepts to design and operate cyber-physical systems. A promising approach, which has been discovered recently as key technology by several industries is the Digital Twin (DT) concept. A DT connects the virtual representation of a physical object, system or process by available information and sensor data streams, which allows to gather new information about the system it mirrors by applying analytic functions. Thereby the DT technology can help to fill sensor data gaps, e. g., to support anomaly detection, and to predict future operating conditions and system states. This paper discusses a dynamic power system DT as a cornerstone instance of a new generation of EMS, and a prospective new EMS architecture, to support the increasingly complex operation of electric power systems. Unlike in traditional offline power system models, the parameters are updated dynamically using measurement information from the supervisory control and data acquisition (SCADA) and a wide area monitoring system (WAMS) to tune the model. This allows to derive a highly accurate virtual representation of the mirrored physical objects. A simulation engine, the Digital Dynamic Mirror (DDM) is introduced, in order to be able to reproduce the state of a reference network in real-time. The validation of the approach is carried out by a case study. In a closed loop within EMS applications, the DDM can help to assess contingency mitigation strategies, thus it can support the decision-making process under variable system conditions. The next generation of control centre Energy Management System (EMS) can benefit from this development by augmentation of the dynamic observability, and the rise of operator situation awareness.","accessed":{"date-parts":[["2022",3,8]]},"author":[{"family":"Brosinsky","given":"Christoph"},{"family":"Krebs","given":"Rainer"},{"family":"Westermann","given":"Dirk"}],"citation-key":"brosinskyEmbeddedDigitalTwins2020","container-title":"At-Automatisierungstechnik","container-title-short":"AT-Autom.","DOI":"10.1515/auto-2020-0086","event-place":"Berlin","ISSN":"0178-2312","issue":"9","issued":{"date-parts":[["2020",9]]},"language":"English","note":"WOS:000565120800005","page":"750-764","publisher":"Walter De Gruyter Gmbh","publisher-place":"Berlin","source":"Web of Science Nextgen","title":"Embedded Digital Twins in future energy management systems: paving the way for automated grid control","title-short":"Embedded Digital Twins in future energy management systems","type":"article-journal","URL":"http://www.webofscience.com/wos/woscc/summary/marked/relevance/1?markedListId=List%202","volume":"68"},
  {"id":"brosinskyFortunateDecisionThat2024","abstract":"Power system operation is gaining complexity due to the changes imposed by the energy transition. Especially, the increased share of intermittent and decentralized renewable generation units in the energy mix, an increased uncertainty regarding the supply of energy, and the predominantly market-driven cross-region and cross-border transport of electricity impose new challenges on the operation of power systems in Europe. In particular, power system operators must facilitate higher utilization of the grid capacity and coordinate more with neighboring transmission system operators (TSOs) and distribution system operators (DSOs). To deal with these new challenges, there is a pressing need to improve the observability and controllability of key system parameters to safeguard the reliability of power systems. Furthermore, the aforementioned developments and challenges go hand in hand with the need to improve the system resilience from the cybersecurity and system stability points of view. In the future, these challenges cannot be met without innovation towards intelligent decision support systems and assistant functions, which allow a look ahead combined with fast response and proactive actions. Here, the rather novel digital twin (DT) concept in combination with data-driven (i.e., machine learning) applications can be purposefully applied.","accessed":{"date-parts":[["2024",3,13]]},"author":[{"family":"Brosinsky","given":"Christoph"},{"family":"Naglič","given":"Matija"},{"family":"Lehnhoff","given":"Sebastian"},{"family":"Krebs","given":"Rainer"},{"family":"Westermann","given":"Dirk"}],"citation-key":"brosinskyFortunateDecisionThat2024","container-title":"IEEE Power and Energy Magazine","DOI":"10.1109/MPE.2023.3330120","ISSN":"1558-4216","issue":"1","issued":{"date-parts":[["2024",1]]},"page":"24-34","source":"IEEE Xplore","title":"A Fortunate Decision That You Can Trust: Digital Twins as Enablers for the Next Generation of Energy Management Systems and Sophisticated Operator Assistance Systems","title-short":"A Fortunate Decision That You Can Trust","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/10398577/","volume":"22"},
+  {"id":"bruntonControlBootcampIntroduction","abstract":"This video motivates robust control with the famous 1978 paper by John Doyle, titled \"Guaranteed Margins for LQG Regulators\"... Abstract:  There are none.  C...","accessed":{"date-parts":[["2024",10,9]]},"citation-key":"bruntonControlBootcampIntroduction","director":[{"family":"Brunton","given":"Steven L."}],"language":"en","source":"www.youtube.com","title":"Control Bootcamp: Introduction to Robust Control","title-short":"Control Bootcamp","type":"motion_picture","URL":"https://www.youtube.com/watch?v=Y6MRgg_TGy0"},
  {"id":"BuildingMathematicalLibrary2020","abstract":"A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field.","accessed":{"date-parts":[["2024",1,28]]},"citation-key":"BuildingMathematicalLibrary2020","issued":{"date-parts":[["2020",10,1]]},"title":"Building the Mathematical Library of the Future","type":"webpage","URL":"https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/"},
  {"id":"bukkapatnamForecastingEvolutionNonlinear2010","abstract":"An approach based on combining nonparametric Gaussian process (GP) modeling with certain local topological considerations is presented for prediction (one-step look ahead) of complex physical systems that exhibit nonlinear and nonstationary dynamics. The key idea here is to partition system trajectories into multiple near-stationary segments by aligning the boundaries of the partitions with those of the piecewise affine projections of the underlying dynamic system, and deriving nonparametric prediction models within each segment. Such an alignment is achieved through the consideration of recurrence and other local topological properties of the underlying system. This approach was applied for state and performance forecasting in Lorenz system under different levels of induced noise and nonstationarity, synthetic heart-rate signals, and a real-world time-series from an industrial operation known to exhibit highly nonlinear and nonstationary dynamics. The results show that local Gaussian process can significantly outperform not just classical system identification, neural network and nonparametric models, but also the sequential Bayesian Monte Carlo methods in terms of prediction accuracy and computational speed.","accessed":{"date-parts":[["2022",4,21]]},"author":[{"family":"Bukkapatnam","given":"Satish T. S."},{"family":"Cheng","given":"Changqing"}],"citation-key":"bukkapatnamForecastingEvolutionNonlinear2010","container-title":"Physical Review E","container-title-short":"Phys. Rev. E","DOI":"10.1103/PhysRevE.82.056206","issue":"5","issued":{"date-parts":[["2010",11,15]]},"page":"056206","publisher":"American Physical Society","source":"APS","title":"Forecasting the evolution of nonlinear and nonstationary systems using recurrence-based local Gaussian process models","type":"article-journal","URL":"https://link.aps.org/doi/10.1103/PhysRevE.82.056206","volume":"82"},
-  {"id":"bullockHardwareintheloopSimulation2004","abstract":"The current generation of macroscopic and microscopic simulation packages do not have control algorithms that incorporate many of the advanced features now available in commercial traffic control hardware. Consequently, there is a need to develop cost effective procedures for evaluating state of the practice traffic signal control equipment so that informed deployment and design decisions can be made. These same procedures can also be used by researchers to develop new algorithms for applications such as transit priority or adaptive control. In order to achieve that objective, this paper presents the motivation for using hardware-in-the-loop simulation procedures. Hardware-in-the-loop simulation presents a new set of challenges for traffic engineering model developers as the “correctness” of a real-time model not only depends upon the numerical computation, but the timeliness with which the simulation model interacts with external control equipment. This paper reviews the state of practice, summarizes the fundamental technologies necessary for implementing such a system, and uses a simple statistical test for assessing the real-time errors introduced into a simulation model.","accessed":{"date-parts":[["2024",8,8]]},"author":[{"family":"Bullock","given":"Darcy"},{"family":"Johnson","given":"Brian"},{"family":"Wells","given":"Richard B."},{"family":"Kyte","given":"Michael"},{"family":"Li","given":"Zhen"}],"citation-key":"bullockHardwareintheloopSimulation2004","container-title":"Transportation Research Part C: Emerging Technologies","container-title-short":"Transportation Research Part C: Emerging Technologies","DOI":"10.1016/j.trc.2002.10.002","ISSN":"0968-090X","issue":"1","issued":{"date-parts":[["2004",2,1]]},"page":"73-89","source":"ScienceDirect","title":"Hardware-in-the-loop simulation","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/S0968090X03000792","volume":"12"},
+  {"id":"bullockHardwareloopSimulation2004","abstract":"The current generation of macroscopic and microscopic simulation packages do not have control algorithms that incorporate many of the advanced features now available in commercial traffic control hardware. Consequently, there is a need to develop cost effective procedures for evaluating state of the practice traffic signal control equipment so that informed deployment and design decisions can be made. These same procedures can also be used by researchers to develop new algorithms for applications such as transit priority or adaptive control. In order to achieve that objective, this paper presents the motivation for using hardware-in-the-loop simulation procedures. Hardware-in-the-loop simulation presents a new set of challenges for traffic engineering model developers as the “correctness” of a real-time model not only depends upon the numerical computation, but the timeliness with which the simulation model interacts with external control equipment. This paper reviews the state of practice, summarizes the fundamental technologies necessary for implementing such a system, and uses a simple statistical test for assessing the real-time errors introduced into a simulation model.","accessed":{"date-parts":[["2024",8,8]]},"author":[{"family":"Bullock","given":"Darcy"},{"family":"Johnson","given":"Brian"},{"family":"Wells","given":"Richard B."},{"family":"Kyte","given":"Michael"},{"family":"Li","given":"Zhen"}],"citation-key":"bullockHardwareloopSimulation2004","container-title":"Transportation Research Part C: Emerging Technologies","container-title-short":"Transportation Research Part C: Emerging Technologies","DOI":"10.1016/j.trc.2002.10.002","ISSN":"0968-090X","issue":"1","issued":{"date-parts":[["2004",2,1]]},"page":"73-89","source":"ScienceDirect","title":"Hardware-in-the-loop simulation","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/S0968090X03000792","volume":"12"},
  {"id":"busoniuApproximateDynamicProgramming2010","abstract":"Dynamic Programming (DP) and Reinforcement Learning (RL) can be used to address problems from a variety of ﬁelds, including automatic control, artiﬁcial intelligence, operations research, and economy. Many problems in these ﬁelds are described by continuous variables, whereas DP and RL can ﬁnd exact solutions only in the discrete case. Therefore, approximation is essential in practical DP and RL. This chapter provides an in-depth review of the literature on approximate DP and RL in large or continuous-space, inﬁnite-horizon problems. Value iteration, policy iteration, and policy search approaches are presented in turn. Model-based (DP) as well as online and batch model-free (RL) algorithms are discussed. We review theoretical guarantees on the approximate solutions produced by these algorithms. Numerical examples illustrate the behavior of several representative algorithms in practice. Techniques to automatically derive value function approximators are discussed, and a comparison between value iteration, policy iteration, and policy search is provided. The chapter closes with a discussion of open issues and promising research directions in approximate DP and RL.","accessed":{"date-parts":[["2024",4,20]]},"author":[{"family":"Buşoniu","given":"Lucian"},{"family":"De Schutter","given":"Bart"},{"family":"Babuška","given":"Robert"}],"citation-key":"busoniuApproximateDynamicProgramming2010","collection-editor":[{"family":"Kacprzyk","given":"Janusz"}],"container-title":"Interactive Collaborative Information Systems","DOI":"10.1007/978-3-642-11688-9_1","editor":[{"family":"Babuška","given":"Robert"},{"family":"Groen","given":"Frans C. A."}],"event-place":"Berlin, Heidelberg","ISBN":"978-3-642-11687-2 978-3-642-11688-9","issued":{"date-parts":[["2010"]]},"language":"en","page":"3-44","publisher":"Springer Berlin Heidelberg","publisher-place":"Berlin, Heidelberg","source":"DOI.org (Crossref)","title":"Approximate Dynamic Programming and Reinforcement Learning","type":"chapter","URL":"http://link.springer.com/10.1007/978-3-642-11688-9_1","volume":"281"},
  {"id":"calc","abstract":"The calc package reimplements the LATEX commands \\setcounter, \\addtocounter, \\setlength, and \\addtolength. Instead of a simple value, these commands now accept an infix notation expression.","author":[{"family":"Thorup","given":"Kresten Krab"},{"family":"Jensen","given":"Frank"},{"family":"Rowley","given":"Chris"}],"citation-key":"calc","language":"en","page":"17","source":"Zotero","title":"The calc package Infix notation arithmetic in LaTeX","type":"article-journal"},
  {"id":"CalculusConstructions2023","abstract":"In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants.\nSome of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity).","accessed":{"date-parts":[["2024",2,22]]},"citation-key":"CalculusConstructions2023","container-title":"Wikipedia","issued":{"date-parts":[["2023",12,30]]},"language":"en","license":"Creative Commons Attribution-ShareAlike License","note":"Page Version ID: 1192670368","source":"Wikipedia","title":"Calculus of constructions","type":"entry-encyclopedia","URL":"https://en.wikipedia.org/w/index.php?title=Calculus_of_constructions&oldid=1192670368"},
@ -179,6 +181,7 @@
  {"id":"CompfilesREADMEMd","accessed":{"date-parts":[["2024",3,28]]},"citation-key":"CompfilesREADMEMd","title":"compfiles/README.md at main · dwrensha/compfiles","type":"webpage","URL":"https://github.com/dwrensha/compfiles/blob/main/README.md"},
  {"id":"ComputerArithmeticFormal2017","accessed":{"date-parts":[["2024",1,16]]},"citation-key":"ComputerArithmeticFormal2017","container-title":"Floating-Point Algorithms and Formal Proofs","DOI":"10.1016/B978-1-78548-112-3.50010-2","ISBN":"978-1-78548-112-3","issued":{"date-parts":[["2017"]]},"language":"en","page":"i-iii","publisher":"Elsevier","source":"DOI.org (Crossref)","title":"Computer Arithmetic and Formal Proofs","type":"chapter","URL":"https://linkinghub.elsevier.com/retrieve/pii/B9781785481123500102"},
  {"id":"contiSidechannelAttacksMobile2022","abstract":"The attacks that leverage the side-channels produced by processes running on mobile and IoT devices are a concrete threat for cyber–physical systems. This special issue is focused on the most recent research work that investigates novel aspects of this topic. This editorial summarizes the contributions of the seven accepted papers for this special issue.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Conti","given":"Mauro"},{"family":"Losiouk","given":"Eleonora"},{"family":"Poovendran","given":"Radha"},{"family":"Spolaor","given":"Riccardo"}],"citation-key":"contiSidechannelAttacksMobile2022","container-title":"Computer Networks","container-title-short":"Computer Networks","DOI":"10.1016/j.comnet.2022.108858","ISSN":"1389-1286","issued":{"date-parts":[["2022",4,22]]},"page":"108858","source":"ScienceDirect","title":"Side-channel attacks on mobile and IoT devices for Cyber–Physical systems","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/S138912862200069X","volume":"207"},
+  {"id":"ControlCOVID19System","accessed":{"date-parts":[["2024",10,1]]},"citation-key":"ControlCOVID19System","title":"Control of COVID-19 system using a novel nonlinear robust control algorithm - ScienceDirect","type":"webpage","URL":"https://www.sciencedirect.com/science/article/pii/S1746809420304341?via%3Dihub"},
  {"id":"controltutorialsformatlab&simulinkInvertedPendulumSystem","accessed":{"date-parts":[["2023",11,15]]},"author":[{"family":"Control Tutorials For Matlab & Simulink","given":""}],"citation-key":"controltutorialsformatlab&simulinkInvertedPendulumSystem","container-title":"Control Tutorials For Matlab & Simulink","genre":"Tutorial","title":"Inverted Pendulum: System Modeling","type":"webpage","URL":"https://ctms.engin.umich.edu/CTMS/index.php?example=InvertedPendulum&section=SystemModeling"},
  {"id":"ConvergenceFacilitatingTransdisciplinary2014","accessed":{"date-parts":[["2024",1,26]]},"citation-key":"ConvergenceFacilitatingTransdisciplinary2014","DOI":"10.17226/18722","event-place":"Washington, D.C.","ISBN":"978-0-309-30151-0","issued":{"date-parts":[["2014",6,16]]},"language":"en","page":"18722","publisher":"National Academies Press","publisher-place":"Washington, D.C.","source":"DOI.org (Crossref)","title":"Convergence: Facilitating Transdisciplinary Integration of Life Sciences, Physical Sciences, Engineering, and Beyond","title-short":"Convergence","type":"book","URL":"http://www.nap.edu/catalog/18722"},
  {"id":"cookIndustrialControlSystem2017","abstract":"The threat to Industrial Control Systems (ICS) from cyber attacks is widely acknowledged by governments and literature. Operators of ICS are looking to address these threats in an effective and cost-sensitive manner that does not expose their operations to additional risks through invasive testing. Whilst existing standards and guidelines offer comprehensive advice for reviewing the security of ICS infrastructure, resource and time limitations can lead to incomplete assessments or undesirably long countermeasure implementation schedules. In this paper we consider the problem of undertaking efﬁcient cyber security risk assessments and implementing mitigations in large, established ICS operations for which a full security review cannot be implemented on a constrained timescale. The contribution is the Industrial Control System Cyber Defence Triage Process (ICS-CDTP). ICS-CDTP determines areas of priority where the impact of attacks is greatest, and where initial investment reduces the organisation’s overall exposure swiftly. ICS-CDTP is designed to be a precursor to a wider, holistic review across the operation following established security management approaches. ICS-CDTP is a novel combination of the Diamond Model of Intrusion Analysis, the Mandiant Attack Lifecycle, and the CARVER Matrix, allowing for an effective triage of attack vectors and likely targets for a capable antagonist. ICS-CDTP identiﬁes and focuses on key ICS processes and their exposure to cyber threats with the view to maintain critical operations. The article deﬁnes ICS-CDTP and exempliﬁes its application using a ﬁctitious water treatment facility, and explains its evaluation as part of a large-scale serious game exercise.","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Cook","given":"Allan"},{"family":"Janicke","given":"Helge"},{"family":"Smith","given":"Richard"},{"family":"Maglaras","given":"Leandros"}],"citation-key":"cookIndustrialControlSystem2017","container-title":"Computers & Security","container-title-short":"Computers & Security","DOI":"10.1016/j.cose.2017.07.009","ISSN":"01674048","issued":{"date-parts":[["2017",9]]},"language":"en","page":"467-481","source":"DOI.org (Crossref)","title":"The industrial control system cyber defence triage process","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S0167404817301505","volume":"70"},
@ -226,15 +229,20 @@
  {"id":"diggaralaVerificationAnnotatedModels","author":[{"family":"Diggarala","given":""},{"family":"Mitra","given":""},{"family":"Visawnathan","given":""}],"citation-key":"diggaralaVerificationAnnotatedModels","container-title":"EMSOFT 2023","title":"Verification of Annotated Models from Executions","type":"paper-conference"},
  {"id":"DigitalTwins","abstract":"Digital Twins","accessed":{"date-parts":[["2024",5,21]]},"citation-key":"DigitalTwins","container-title":"NRC Web","language":"en-US","title":"Digital Twins","type":"webpage","URL":"https://www.nrc.gov/reactors/power/digital-twins.html"},
  {"id":"dingSurveySecurityControl2018","abstract":"Cyber-physical systems (CPSs), which are an integration of computation, networking, and physical processes, play an increasingly important role in critical infrastructure, government and everyday life. Due to physical constraints, embedded computers and networks may give rise to some additional security vulnerabilities, which results in losses of enormous economy benefits or disorder of social life. As a result, it is of significant to properly investigate the security issue of CPSs to ensure that such systems are operating in a safe manner. This paper, from a control theory perspective, presents an overview of recent advances on security control and attack detection of industrial CPSs. First, the typical system modeling on CPSs is summarized to cater for the requirement of the performance analysis. Then three typical types of cyber-attacks, i.e. denial-of-service attacks, replay attacks, and deception attacks, are disclosed from an engineering perspective. Moreover, robustness, security and resilience as well as stability are discussed to govern the capability of weakening various attacks. The development on attack detection for industrial CPSs is reviewed according to the categories on detection approaches. Furthermore, the security control and state estimation are discussed in detail. Finally, some challenge issues are raised for the future research. (c) 2017 Elsevier B.V. All rights reserved.","accessed":{"date-parts":[["2022",3,8]]},"author":[{"family":"Ding","given":"Derui"},{"family":"Han","given":"Qing-Long"},{"family":"Xiang","given":"Yang"},{"family":"Ge","given":"Xiaohua"},{"family":"Zhang","given":"Xian-Ming"}],"citation-key":"dingSurveySecurityControl2018","container-title":"Neurocomputing","container-title-short":"Neurocomputing","DOI":"10.1016/j.neucom.2017.10.009","event-place":"Amsterdam","ISSN":"0925-2312","issued":{"date-parts":[["2018",1,31]]},"language":"English","note":"WOS:000418370200157","page":"1674-1683","publisher":"Elsevier","publisher-place":"Amsterdam","source":"Web of Science Nextgen","title":"A survey on security control and attack detection for industrial cyber-physical systems","type":"article-journal","URL":"http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&amp;SrcAuth=DOISource&amp;SrcApp=WOS&amp;KeyAID=10.1016%2Fj.neucom.2017.10.009&amp;DestApp=DOI&amp;SrcAppSID=8COHllwH67CX3cigLe5&amp;SrcJTitle=NEUROCOMPUTING&amp;DestDOIRegistrantName=Elsevier","volume":"275"},
+  {"id":"djeziriRobustMonitoringElectric2009","abstract":"This paper deals with a robust fault-detection and isolation (FDI) technique, which is applied to the traction system of an electric vehicle, in the presence of structured and unstructured uncertainties. Due to the structural and multidomain properties of the bond graph, the generation of a nonlinear model and residuals for the studied system with adaptive thresholds is synthesized. The parameters and structured uncertainties are identified by using a least-square algorithm. A super-twisting observer is used to estimate both unstructured uncertainties and unknown inputs. Cosimulation with real experimental data shows the robustness of the residuals to the considered uncertainties and their sensitivity to the faults.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Djeziri","given":"Mohand Arab"},{"family":"Merzouki","given":"Rochdi"},{"family":"Bouamama","given":"Belkacem Ould"}],"citation-key":"djeziriRobustMonitoringElectric2009","container-title":"IEEE Transactions on Vehicular Technology","DOI":"10.1109/TVT.2009.2026281","ISSN":"1939-9359","issue":"9","issued":{"date-parts":[["2009",11]]},"page":"4710-4719","source":"IEEE Xplore","title":"Robust Monitoring of an Electric Vehicle With Structured and Unstructured Uncertainties","type":"article-journal","URL":"https://ieeexplore.ieee.org/abstract/document/5130067?casa_token=mNjsfmKFCA4AAAAA:TxD0lmASLKB2CjqWYyaFLWCZCFE4bjaBqDuytDLbrGtMzeUAtVd64ulSh_WGNjKOcGhL7IGaHA","volume":"58"},
  {"id":"DoDCyberWorkforce","accessed":{"date-parts":[["2023",11,7]]},"citation-key":"DoDCyberWorkforce","title":"DoD Cyber Workforce Framework – DoD Cyber Exchange","type":"webpage","URL":"https://public.cyber.mil/wid/dcwf/"},
  {"id":"DOE-TRL","author":[{"literal":"Office of Project Management Oversight & Assessments"}],"citation-key":"DOE-TRL","issued":{"date-parts":[["2011"]]},"number":"DOE G 413.3-4A","publisher":"U.S. Department of Energy","title":"Technology readiness assessment guide","type":"report"},
  {"id":"dollnerGeospatialArtificialIntelligence2020","abstract":"Artificial intelligence (AI) is changing fundamentally the way how IT solutions are implemented and operated across all application domains, including the geospatial domain. This contribution outlines AI-based techniques for 3D point clouds and geospatial digital twins as generic components of geospatial AI. First, we briefly reflect on the term “AI” and outline technology developments needed to apply AI to IT solutions, seen from a software engineering perspective. Next, we characterize 3D point clouds as key category of geodata and their role for creating the basis for geospatial digital twins; we explain the feasibility of machine learning (ML) and deep learning (DL) approaches for 3D point clouds. In particular, we argue that 3D point clouds can be seen as a corpus with similar properties as natural language corpora and formulate a “Naturalness Hypothesis” for 3D point clouds. In the main part, we introduce a workflow for interpreting 3D point clouds based on ML/ DL approaches that derive domain-specific and application-specific semantics for 3D point clouds without having to create explicit spatial 3D models or explicit rule sets. Finally, examples are shown how ML/DL enables us to efficiently build and maintain base data for geospatial digital twins such as virtual 3D city models, indoor models, or building information models.","accessed":{"date-parts":[["2022",3,2]]},"author":[{"family":"Döllner","given":"Jürgen"}],"citation-key":"dollnerGeospatialArtificialIntelligence2020","container-title":"PFG – Journal of Photogrammetry, Remote Sensing and Geoinformation Science","container-title-short":"PFG","DOI":"10.1007/s41064-020-00102-3","ISSN":"2512-2789, 2512-2819","issue":"1","issued":{"date-parts":[["2020",2]]},"language":"en","page":"15-24","source":"DOI.org (Crossref)","title":"Geospatial Artificial Intelligence: Potentials of Machine Learning for 3D Point Clouds and Geospatial Digital Twins","title-short":"Geospatial Artificial Intelligence","type":"article-journal","URL":"http://link.springer.com/10.1007/s41064-020-00102-3","volume":"88"},
+  {"id":"doyleFeedbackControlTheory2009","abstract":"In any system, if there exists a linear relationship between two variables, then it is said that it is a linear system.","author":[{"family":"Doyle","given":"John"},{"family":"A","given":"Francis"},{"family":"Tannenbaum","given":"Allen"}],"citation-key":"doyleFeedbackControlTheory2009","DOI":"10.1007/978-0-387-85460-1_1","issued":{"date-parts":[["2009",1,1]]},"source":"ResearchGate","title":"Feedback Control Theory","type":"book"},
+  {"id":"doyleGuaranteedMarginsLQG1978","abstract":"There are none.","accessed":{"date-parts":[["2024",10,9]]},"author":[{"family":"Doyle","given":"J."}],"citation-key":"doyleGuaranteedMarginsLQG1978","container-title":"IEEE Transactions on Automatic Control","DOI":"10.1109/TAC.1978.1101812","ISSN":"1558-2523","issue":"4","issued":{"date-parts":[["1978",8]]},"page":"756-757","source":"IEEE Xplore","title":"Guaranteed margins for LQG regulators","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/1101812","volume":"23"},
  {"id":"dragos2020","abstract":"Today we published our 2020 ICS Cybersecurity Year in Review report, an annual analysis of Industrial Control System (ICS)/Operational Technology (OT) focused cyber threats, vulnerabilities, assessments, and incident response insights. The ICS/OT community has long struggled with a lack of public insights into these types of problem areas. It is Dragos’s goal to share the observations and lessons learned with the industrial community for data-driven analysis and...","accessed":{"date-parts":[["2022",3,25]]},"citation-key":"dragos2020","issued":{"date-parts":[["2021",2,24]]},"language":"en-US","title":"2020 ICS Cybersecurity Year in Review | Dragos","type":"webpage","URL":"https://www.dragos.com/blog/industry-news/2020-ics-cybersecurity-year-in-review/"},
  {"id":"dreierFormallyPracticallyVerifying2019","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Dreier","given":"Jannik"},{"family":"Puys","given":"Maxime"},{"family":"Potet","given":"Marie-Laure"},{"family":"Lafourcade","given":"Pascal"},{"family":"Roch","given":"Jean-Louis"}],"citation-key":"dreierFormallyPracticallyVerifying2019","container-title":"Computers & Security","container-title-short":"Computers & Security","DOI":"10.1016/j.cose.2018.09.018","ISSN":"01674048","issued":{"date-parts":[["2019",9]]},"language":"en","page":"453-470","source":"DOI.org (Crossref)","title":"Formally and practically verifying flow properties in industrial systems","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S016740481831441X","volume":"86"},
  {"id":"DSPACE","abstract":"Around the world, dSPACE helps companies make their visions and ideas come to life faster and more reliably. In this we take pride. We are your partner in simulation and validation.","accessed":{"date-parts":[["2024",8,14]]},"citation-key":"DSPACE","language":"en","title":"dSPACE","type":"webpage","URL":"https://www.dspace.com/en/inc/home.cfm"},
  {"id":"duggiralaC2E2VerificationTool2015","abstract":"Mathwork’s Stateﬂow is a predominant environment for modeling embedded and cyberphysical systems where control software interact with physical processes. We present Compare-Execute-Check-Engine (C2E2)—a veriﬁcation tool for continuous and hybrid Stateﬂow models. It checks bounded time invariant properties of models with nonlinear dynamics, and discrete transitions with guards and resets. C2E2 transforms the model, computing simulations using a validated numerical solver, and then computes reachtube over-approximations with increasing precision. For this last step it uses annotations that have to be added to the model. These annotations are extensions of proof certiﬁcates studied in Control Theory and can be automatically obtained for linear dynamics. The C2E2 algorithm is sound and it is guaranteed to terminate if the system is robustly safe (or unsafe) with respect to perturbations to the of guards and invariants of the model. We present the architecture of C2E2, its workﬂow, and examples illustrating its potential role in model-based design, veriﬁcation, and validation.","accessed":{"date-parts":[["2023",11,2]]},"author":[{"family":"Duggirala","given":"Parasara Sridhar"},{"family":"Mitra","given":"Sayan"},{"family":"Viswanathan","given":"Mahesh"},{"family":"Potok","given":"Matthew"}],"citation-key":"duggiralaC2E2VerificationTool2015","container-title":"Tools and Algorithms for the Construction and Analysis of Systems","DOI":"10.1007/978-3-662-46681-0_5","editor":[{"family":"Baier","given":"Christel"},{"family":"Tinelli","given":"Cesare"}],"event-place":"Berlin, Heidelberg","ISBN":"978-3-662-46680-3 978-3-662-46681-0","issued":{"date-parts":[["2015"]]},"language":"en","page":"68-82","publisher":"Springer Berlin Heidelberg","publisher-place":"Berlin, Heidelberg","source":"DOI.org (Crossref)","title":"C2E2: A Verification Tool for Stateflow Models","title-short":"C2E2","type":"chapter","URL":"http://link.springer.com/10.1007/978-3-662-46681-0_5","volume":"9035"},
  {"id":"duLearningUniversalPolicies2023","abstract":"A goal of artificial intelligence is to construct an agent that can solve a wide variety of tasks. Recent progress in text-guided image synthesis has yielded models with an impressive ability to generate complex novel images, exhibiting combinatorial generalization across domains. Motivated by this success, we investigate whether such tools can be used to construct more general-purpose agents. Specifically, we cast the sequential decision making problem as a text-conditioned video generation problem, where, given a text-encoded specification of a desired goal, a planner synthesizes a set of future frames depicting its planned actions in the future, after which control actions are extracted from the generated video. By leveraging text as the underlying goal specification, we are able to naturally and combinatorially generalize to novel goals. The proposed policy-as-video formulation can further represent environments with different state and action spaces in a unified space of images, which, for example, enables learning and generalization across a variety of robot manipulation tasks. Finally, by leveraging pretrained language embeddings and widely available videos from the internet, the approach enables knowledge transfer through predicting highly realistic video plans for real robots.","accessed":{"date-parts":[["2023",10,5]]},"author":[{"family":"Du","given":"Yilun"},{"family":"Yang","given":"Mengjiao"},{"family":"Dai","given":"Bo"},{"family":"Dai","given":"Hanjun"},{"family":"Nachum","given":"Ofir"},{"family":"Tenenbaum","given":"Joshua B."},{"family":"Schuurmans","given":"Dale"},{"family":"Abbeel","given":"Pieter"}],"citation-key":"duLearningUniversalPolicies2023","issued":{"date-parts":[["2023",2,1]]},"language":"en","number":"arXiv:2302.00111","publisher":"arXiv","source":"arXiv.org","title":"Learning Universal Policies via Text-Guided Video Generation","type":"article","URL":"http://arxiv.org/abs/2302.00111"},
  {"id":"durethConditionalDiffusionbasedMicrostructure2023","accessed":{"date-parts":[["2024",5,20]]},"author":[{"family":"Düreth","given":"Christian"},{"family":"Seibert","given":"Paul"},{"family":"Rücker","given":"Dennis"},{"family":"Handford","given":"Stephanie"},{"family":"Kästner","given":"Markus"},{"family":"Gude","given":"Maik"}],"citation-key":"durethConditionalDiffusionbasedMicrostructure2023","container-title":"Materials Today Communications","container-title-short":"Materials Today Communications","DOI":"10.1016/j.mtcomm.2023.105608","ISSN":"23524928","issued":{"date-parts":[["2023",6]]},"language":"en","page":"105608","source":"DOI.org (Crossref)","title":"Conditional diffusion-based microstructure reconstruction","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S2352492823002982","volume":"35"},
+  {"id":"durethConditionalDiffusionbasedMicrostructure2023a","abstract":"Microstructure reconstruction, a major component of inverse computational materials engineering, is currently advancing at an unprecedented rate. While various training-based and training-free approaches are developed, the majority of contributions are based on generative adversarial networks. In contrast, diffusion models constitute a more stable alternative, which have recently become the new state of the art and currently attract much attention. The present work investigates the applicability of diffusion models to the reconstruction of real-world microstructure data. For this purpose, a highly diverse and morphologically complex data set is created by combining and processing databases from the literature, where the reconstruction of realistic micrographs for a given material class demonstrates the ability of the model to capture these features. Furthermore, a fiber composite data set is used to validate the applicability of diffusion models to small data set sizes that can realistically be created by a single lab. The quality and diversity of the reconstructed microstructures is quantified by means of descriptor-based error metrics as well as the Fréchet inception distance (FID) score. Although not present in the training data set, the generated samples are visually indistinguishable from real data to the untrained eye and various error metrics are computed. This demonstrates the utility of diffusion models in microstructure reconstruction and provides a basis for further extensions such as 2D-to-3D reconstruction or application to multiscale modeling and structure–property linkages.","accessed":{"date-parts":[["2024",10,1]]},"author":[{"family":"Düreth","given":"Christian"},{"family":"Seibert","given":"Paul"},{"family":"Rücker","given":"Dennis"},{"family":"Handford","given":"Stephanie"},{"family":"Kästner","given":"Markus"},{"family":"Gude","given":"Maik"}],"citation-key":"durethConditionalDiffusionbasedMicrostructure2023a","container-title":"Materials Today Communications","container-title-short":"Materials Today Communications","DOI":"10.1016/j.mtcomm.2023.105608","ISSN":"2352-4928","issued":{"date-parts":[["2023",6,1]]},"page":"105608","source":"ScienceDirect","title":"Conditional diffusion-based microstructure reconstruction","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/S2352492823002982","volume":"35"},
+  {"id":"duriezMachineLearningControl2017","accessed":{"date-parts":[["2024",10,9]]},"author":[{"family":"Duriez","given":"Thomas"},{"family":"Brunton","given":"Steven L."},{"family":"Noack","given":"Bernd R."}],"citation-key":"duriezMachineLearningControl2017","collection-title":"Fluid Mechanics and Its Applications","DOI":"10.1007/978-3-319-40624-4","event-place":"Cham","ISBN":"978-3-319-40623-7 978-3-319-40624-4","issued":{"date-parts":[["2017"]]},"language":"en","license":"http://www.springer.com/tdm","publisher":"Springer International Publishing","publisher-place":"Cham","source":"DOI.org (Crossref)","title":"Machine Learning Control – Taming Nonlinear Dynamics and Turbulence","type":"book","URL":"http://link.springer.com/10.1007/978-3-319-40624-4","volume":"116"},
  {"id":"dutertreFormalModelingAnalysis2007","abstract":"Modbus is a communication protocol that is widely used in SCADA systems and distributed control applications. This paper presents formal speciﬁcations of Modbus developed using PVS, a generic theorem prover; and SAL, a toolset for the automatic analysis of state-transition systems. Both formalizations are based on the Modbus Application Protocol, which speciﬁes the format of Modbus request and response messages. This formal modeling eﬀort is the ﬁrst step in the development of automated methods for systematic and extensive testing of Modbus devices.","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Dutertre","given":"Bruno"}],"citation-key":"dutertreFormalModelingAnalysis2007","container-title":"Critical Infrastructure Protection","DOI":"10.1007/978-0-387-75462-8_14","editor":[{"family":"Goetz","given":"Eric"},{"family":"Shenoi","given":"Sujeet"}],"event-place":"Boston, MA","ISBN":"978-0-387-75461-1","issued":{"date-parts":[["2007"]]},"language":"en","page":"189-204","publisher":"Springer US","publisher-place":"Boston, MA","source":"DOI.org (Crossref)","title":"Formal Modeling and Analysis of the Modbus Protocol","type":"chapter","URL":"http://link.springer.com/10.1007/978-0-387-75462-8_14","volume":"253"},
  {"id":"dwDARPAExplainableArtificial2019","author":[{"family":"DW","given":"Gunning D. Aha"}],"citation-key":"dwDARPAExplainableArtificial2019","container-title":"AI Mag","issue":"2","issued":{"date-parts":[["2019"]]},"page":"44","title":"DARPA’s explainable artificial intelligence program","type":"article-journal","volume":"40"},
  {"id":"DyanmicDeceptionIndustrial","citation-key":"DyanmicDeceptionIndustrial","publisher":"Attivo Networks","title":"Dyanmic Deception for Industrial Automation and Control Systems","type":"document","URL":"https://attivonetworks.com/documentation/Attivo_Networks-Energy_Whitepaper.pdf"},
@ -259,6 +267,7 @@
  {"id":"fanAutomaticReachabilityAnalysis2016","abstract":"C2E2 is a bounded reachability analysis tool for nonlinear dynamical systems and hybrid automaton models. Previously it required users to annotate each system of diﬀerential equations of the hybrid automaton with discrepancy functions, and since these annotations are diﬃcult to get for general nonlinear diﬀerential equations, the tool had limited usability. This version of C2E2 is improved in several ways, the most prominent among which is the elimination of the need for userprovided discrepancy functions. It automatically computes piece-wise (or local) discrepancy functions around the reachable parts of the state space using symbolically computed Jacobian matrix and eigenvalue perturbation bounds. The special cases of linear and constant rate diﬀerential equations are handled with more eﬃcient algorithm. In this paper, we discuss these and other new features that make the new C2E2 a usable tool for bounded reachability analysis of hybrid systems.","accessed":{"date-parts":[["2023",11,2]]},"author":[{"family":"Fan","given":"Chuchu"},{"family":"Qi","given":"Bolun"},{"family":"Mitra","given":"Sayan"},{"family":"Viswanathan","given":"Mahesh"},{"family":"Duggirala","given":"Parasara Sridhar"}],"citation-key":"fanAutomaticReachabilityAnalysis2016","container-title":"Computer Aided Verification","DOI":"10.1007/978-3-319-41528-4_29","editor":[{"family":"Chaudhuri","given":"Swarat"},{"family":"Farzan","given":"Azadeh"}],"event-place":"Cham","ISBN":"978-3-319-41527-7 978-3-319-41528-4","issued":{"date-parts":[["2016"]]},"language":"en","page":"531-538","publisher":"Springer International Publishing","publisher-place":"Cham","source":"DOI.org (Crossref)","title":"Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2","type":"chapter","URL":"http://link.springer.com/10.1007/978-3-319-41528-4_29","volume":"9779"},
  {"id":"fanOverviewCybersecurityIndustrial2015","abstract":"With the development of information technology, the network connection of industrial control system (ICS) and information technology (IT) is becoming more and more closely. What’s more, the security issues of traditional IT systems in industrial control system are also more prominent. Early industrial control system mainly uses physical isolation approach to protect security. In this paper, we review the characteristics and reference models of industrial control system and analyze the current security status of industrial control system. Moreover, we propose a defense-in-depth system, security policies of active protection and passive monitoring for these security issues. Besides, we also discuss the key technologies and summarize the full text.","accessed":{"date-parts":[["2022",9,30]]},"author":[{"family":"Fan","given":"Xiaohe"},{"family":"Fan","given":"Kefeng"},{"family":"Wang","given":"Yong"},{"family":"Zhou","given":"Ruikang"}],"citation-key":"fanOverviewCybersecurityIndustrial2015","container-title":"2015 International Conference on Cyber Security of Smart Cities, Industrial Control System and Communications (SSIC)","DOI":"10.1109/SSIC.2015.7245324","event-place":"Shanghai, China","event-title":"2015 International Conference on Cyber Security of Smart cities, Industrial Control System and Communications (SSIC)","ISBN":"978-1-4673-7977-9","issued":{"date-parts":[["2015",8]]},"language":"en","page":"1-7","publisher":"IEEE","publisher-place":"Shanghai, China","source":"DOI.org (Crossref)","title":"Overview of cyber-security of industrial control system","type":"paper-conference","URL":"http://ieeexplore.ieee.org/document/7245324/"},
  {"id":"faruqueDesignMethodologiesSecuring2015","abstract":"Cyber-Physical Systems (CPS) are in most cases safety- and mission-critical. Standard design techniques used for securing embedded systems are not suitable for CPS due to the restricted computation and communication budget available in the latter. In addition, the sensitivity of sensed data and the presence of actuation components further increase the security requirements of CPS. To address these issues, it is necessary to provide new design methods in which security is considered from the beginning of the whole design flow and addressed in a holistic way. In this paper, we focus on the design of secure CPS as part of the complete CPS design process, and provide insights into new requirements on platform-aware design of control components, design methodologies and architectures posed by CPS design. We start by discussing methods for the multi-disciplinary modeling, simulation, tools, and software synthesis challenges for CPS. We also present a framework for design of secure control systems for CPS, while taking into account properties of the underlying computation and communication platforms. Finally, we describe the security challenges in the computing hardware that is used in CPS.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Faruque","given":"Mohammad Al"},{"family":"Regazzoni","given":"Francesco"},{"family":"Pajic","given":"Miroslav"}],"citation-key":"faruqueDesignMethodologiesSecuring2015","container-title":"2015 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS)","DOI":"10.1109/CODESISSS.2015.7331365","event-title":"2015 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS)","issued":{"date-parts":[["2015",10]]},"page":"30-36","source":"IEEE Xplore","title":"Design methodologies for securing cyber-physical systems","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/7331365"},
+  {"id":"farzanRobustControlSynthesis2020","abstract":"Control of wire-borne underactuated brachiating robots requires a robust feedback control design that can deal with dynamic uncertainties, actuator constraints and unmeasurable states. In this paper, we develop a robust feedback control for brachiating on flexible cables, building on previous work on optimal trajectory generation and time-varying LQR controller design. We propose a novel simplified model for approximation of the flexible cable dynamics, which enables inclusion of parametric model uncertainties in the system. We then use semidefinite programming (SDP) and sum-of-squares (SOS) optimization to synthesize a time-varying feedback control with formal robustness guarantees to account for model uncertainties and unmeasurable states in the system. Through simulation, hardware experiments and comparison with a time-varying LQR controller, it is shown that the proposed robust controller results in relatively large robust backward reachable sets and is able to reliably track a pre-generated optimal trajectory and achieve the desired brachiating motion in the presence of parametric model uncertainties, actuator limits, and unobservable states.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Farzan","given":"Siavash"},{"family":"Hu","given":"Ai-Ping"},{"family":"Bick","given":"Michael"},{"family":"Rogers","given":"Jonathan"}],"citation-key":"farzanRobustControlSynthesis2020","container-title":"2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)","DOI":"10.1109/IROS45743.2020.9341348","event-title":"2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)","ISSN":"2153-0866","issued":{"date-parts":[["2020",10]]},"page":"7744-7751","source":"IEEE Xplore","title":"Robust Control Synthesis and Verification for Wire-Borne Underactuated Brachiating Robots Using Sum-of-Squares Optimization","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/9341348?casa_token=rxbMIqFK310AAAAA:nxVupZ3MZnKxYVgYgu1goGtyknCyfF1LjpKYJUbNs154frxsOCGfetfcXIXJZtHaaV4GplE7yQ"},
  {"id":"faselEnsembleSINDyRobustSparse2022","abstract":"Sparse model identification enables the discovery of nonlinear dynamical systems purely from data; however, this approach is sensitive to noise, especially in the low-data limit. In this work, we leverage the statistical approach of bootstrap aggregating (bagging) to robustify the sparse identification of the nonlinear dynamics (SINDy) algorithm. First, an ensemble of SINDy models is identified from subsets of limited and noisy data. The aggregate model statistics are then used to produce inclusion probabilities of the candidate functions, which enables uncertainty quantification and probabilistic forecasts. We apply this ensemble-SINDy (E-SINDy) algorithm to several synthetic and real-world datasets and demonstrate substantial improvements to the accuracy and robustness of model discovery from extremely noisy and limited data. For example, E-SINDy uncovers partial differential equations models from data with more than twice as much measurement noise as has been previously reported. Similarly, E-SINDy learns the Lotka Volterra dynamics from remarkably limited data of yearly lynx and hare pelts collected from 1900 to 1920. E-SINDy is computationally efficient, with similar scaling as standard SINDy. Finally, we show that ensemble statistics from E-SINDy can be exploited for active learning and improved model predictive control.","accessed":{"date-parts":[["2024",1,4]]},"author":[{"family":"Fasel","given":"U."},{"family":"Kutz","given":"J. N."},{"family":"Brunton","given":"B. W."},{"family":"Brunton","given":"S. L."}],"citation-key":"faselEnsembleSINDyRobustSparse2022","container-title":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","container-title-short":"Proc. R. Soc. A.","DOI":"10.1098/rspa.2021.0904","ISSN":"1364-5021, 1471-2946","issue":"2260","issued":{"date-parts":[["2022",4]]},"language":"en","page":"20210904","source":"DOI.org (Crossref)","title":"Ensemble-SINDy: Robust sparse model discovery in the low-data, high-noise limit, with active learning and control","title-short":"Ensemble-SINDy","type":"article-journal","URL":"https://royalsocietypublishing.org/doi/10.1098/rspa.2021.0904","volume":"478"},
  {"id":"fayGaussianProcessModels2017","abstract":"This paper presents a ubiquitous thermal comfort preference learning study in a noisy environment. We introduce Gaussian Process models into this ﬁeld and show they are ideal, allowing rejection of outliers, deadband samples, and produce excellent estimates of a users preference function. In addition, informative combinations of users preferences becomes possible, some of which demonstrate well deﬁned maxima ideal for control signals. Interestingly, while those users studied have diﬀering preferences, their hyperparameters are concentrated allowing priors for new users. In addition, we present an active learning algorithm which estimates when to poll users to maximise the information returned.","accessed":{"date-parts":[["2022",4,21]]},"author":[{"family":"Fay","given":"Damien"},{"family":"O’Toole","given":"Liam"},{"family":"Brown","given":"Kenneth N."}],"citation-key":"fayGaussianProcessModels2017","container-title":"Pervasive and Mobile Computing","container-title-short":"Pervasive and Mobile Computing","DOI":"10.1016/j.pmcj.2016.08.012","ISSN":"15741192","issued":{"date-parts":[["2017",8]]},"language":"en","page":"135-158","source":"DOI.org (Crossref)","title":"Gaussian Process models for ubiquitous user comfort preference sampling; global priors, active sampling and outlier rejection","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S1574119216301651","volume":"39"},
  {"id":"FederalCybersecurityResearch2023","citation-key":"FederalCybersecurityResearch2023","issued":{"date-parts":[["2023"]]},"language":"en","source":"Zotero","title":"Federal Cybersecurity Research and Development Strategic Plan (2023)","type":"article-journal"},
@ -322,6 +331,7 @@
  {"id":"grandeAugmentedNeuralLyapunov2023","abstract":"Machine learning-based methodologies have recently been adapted to solve control problems. The Neural Lyapunov Control (NLC) method is one such example. This approach combines Artificial Neural Networks (ANNs) with Satisfiability Modulo Theories (SMT) solvers to synthesise stabilising control laws and to prove their formal correctness. The ANNs are trained over a dataset of state-space samples to generate candidate control and Lyapunov functions, while the SMT solvers are tasked with certifying the correctness of the Lyapunov function over a continuous domain or by returning a counterexample. Despite the approach’s attractiveness, issues can occur due to subsequent calls of the SMT module at times returning similar counterexamples, which can turn out to be uninformative and may lead to dataset overfitting. Additionally, the control network weights are usually initialised with pre-computed gains from state-feedback controllers, e.g. Linear-Quadratic Regulators. To properly perform the initialisation requires user time and control expertise. In this work, we present an Augmented NLC method that mitigates these drawbacks, removes the need for the control initialisation and further improves counterexample generation. As a result, the proposed method allows the synthesis of nonlinear (as well as linear) control laws with the sole requirement being the knowledge of the system dynamics. The ANLC is tested over challenging benchmarks such as the Lorenz attractor and outperformed existing methods in terms of successful synthesis rate. The developed framework is released open-source at: https://github.com/grande-dev/Augmented-Neural-Lyapunov-Control.","accessed":{"date-parts":[["2024",1,17]]},"author":[{"family":"Grande","given":"Davide"},{"family":"Peruffo","given":"Andrea"},{"family":"Anderlini","given":"Enrico"},{"family":"Salavasidis","given":"Georgios"}],"citation-key":"grandeAugmentedNeuralLyapunov2023","container-title":"IEEE Access","DOI":"10.1109/ACCESS.2023.3291349","ISSN":"2169-3536","issued":{"date-parts":[["2023"]]},"page":"67979-67986","source":"IEEE Xplore","title":"Augmented Neural Lyapunov Control","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/10171339","volume":"11"},
  {"id":"gratzerJozefgLearntt2024","abstract":"A collection of resources for learning type theory and type theory adjacent fields.","accessed":{"date-parts":[["2024",1,22]]},"author":[{"family":"gratzer","given":"daniel"}],"citation-key":"gratzerJozefgLearntt2024","issued":{"date-parts":[["2024",1,21]]},"original-date":{"date-parts":[["2015",8,3]]},"source":"GitHub","title":"jozefg/learn-tt","type":"software","URL":"https://github.com/jozefg/learn-tt"},
  {"id":"grayIndustryuniversityProjectsCenters1986","author":[{"family":"Gray","given":"D. O."},{"family":"Johnson","given":"E. C."},{"family":"Gidley","given":"T. R."}],"citation-key":"grayIndustryuniversityProjectsCenters1986","container-title":"Evaluation Review","issued":{"date-parts":[["1986"]]},"page":"776–793","title":"Industry-university projects and centers: An empirical comparison of two federally-funded models of cooperative science","type":"article-journal","volume":"10"},
+  {"id":"greenLinearRobustControl1995","author":[{"family":"Green","given":"Michael"}],"call-number":"TJ213 G755 1995","citation-key":"greenLinearRobustControl1995","collection-title":"Prentice Hall information and system sciences series","contributor":[{"family":"Limebeer","given":"David J. N."}],"event-place":"Englewood Cliffs, N.J","issued":{"date-parts":[["1995"]]},"language":"eng","number-of-pages":"xv+538","publisher":"Prentice Hall","publisher-place":"Englewood Cliffs, N.J","source":"pitt.primo.exlibrisgroup.com","title":"Linear robust control","type":"book"},
  {"id":"GRID-Institute","author":[{"literal":"GRID Institute"}],"citation-key":"GRID-Institute","issued":{"literal":"Date accessed 11/2021"},"type":"document","URL":"http://grid.pitt.edu/"},
  {"id":"grobelnaGroblena_masterPdf2019","author":[{"family":"Grobelna","given":"Marta"}],"citation-key":"grobelnaGroblena_masterPdf2019","genre":"Master's thesis","issued":{"date-parts":[["2019",9,16]]},"publisher":"RWTH Aachen University","title":"groblena_master.pdf","type":"thesis"},
  {"id":"grochowskiAlgorithmicTransparencyExplainability2021","author":[{"family":"Grochowski","given":"Mateusz"},{"family":"Jablonowska","given":"Agnieszka"},{"family":"Lagioia","given":"Francesca"},{"family":"Sartor","given":"Giovanni"}],"citation-key":"grochowskiAlgorithmicTransparencyExplainability2021","container-title":"Critical Analysis L.","issued":{"date-parts":[["2021"]]},"page":"43","publisher":"HeinOnline","title":"Algorithmic transparency and explainability for EU consumer protection: unwrapping the regulatory premises","type":"article-journal","volume":"8"},
@ -338,9 +348,11 @@
  {"id":"HackExposesVulnerability","accessed":{"date-parts":[["2022",4,2]]},"citation-key":"HackExposesVulnerability","title":"Hack exposes vulnerability of cash-strapped US water plants | AP News","type":"webpage","URL":"https://apnews.com/article/business-water-utilities-florida-coronavirus-pandemic-utilities-e783b0f1ca2af02f19f5a308d44e6abb"},
  {"id":"HackExposesVulnerability2021","abstract":"ST. PETERSBURG, Fla. (AP) — A hacker’s botched attempt to poison the water supply of a small Florida city is raising alarms about just how vulnerable the nation's water systems may be to attacks by more sophisticated intruders...","accessed":{"date-parts":[["2022",4,2]]},"citation-key":"HackExposesVulnerability2021","container-title":"AP NEWS","issued":{"date-parts":[["2021",4,20]]},"language":"en","section":"Water utilities","title":"Hack exposes vulnerability of cash-strapped US water plants","type":"webpage","URL":"https://apnews.com/article/business-water-utilities-florida-coronavirus-pandemic-utilities-e783b0f1ca2af02f19f5a308d44e6abb"},
  {"id":"hadiControlCOVID19System2021","accessed":{"date-parts":[["2024",5,20]]},"author":[{"family":"Hadi","given":"Musadaq A."},{"family":"Ali","given":"Hazem I."}],"citation-key":"hadiControlCOVID19System2021","container-title":"Biomedical Signal Processing and Control","container-title-short":"Biomedical Signal Processing and Control","DOI":"10.1016/j.bspc.2020.102317","ISSN":"17468094","issued":{"date-parts":[["2021",2]]},"language":"en","license":"https://www.elsevier.com/tdm/userlicense/1.0/","page":"102317","source":"DOI.org (Crossref)","title":"Control of COVID-19 system using a novel nonlinear robust control algorithm","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S1746809420304341","volume":"64"},
+  {"id":"hadiControlCOVID19System2021a","abstract":"COVID-19 has been a worldwide concern since the outbreak. Many strategies have been involved such as suppression and mitigation strategies to deal with this epidemic. In this paper, a new mathematical-engineering strategy is introduced in order to control the COVID-19 epidemic. Thereby, control theory is involved in controlling the unstable epidemic alongside with the other suggested strategies until the vaccine will hopefully be invented as soon as possible. A new robust control algorithm is introduced to compensate the COVID-19 nonlinear system by propose a proper controller after using necessary assumptions and analysis are made. In addition, the Variable Transformation Technique (VTT) is used to simplify the COVID-19 system. Furthermore, the Most Valuable Player Algorithm (MVPA) is applied in order to optimize the parameters of the proposed controller. The simulation results are based on the daily reports of two cities Hubei (China) and Lazio (Italy) since the outbreak. It can be concluded that the proposed control algorithm can effectively compensate the COVID-19 system. In addition, it can be considered as an effective mathematical-engineering strategy to control this epidemic alongside with the other strategies.","accessed":{"date-parts":[["2024",10,1]]},"author":[{"family":"Hadi","given":"Musadaq A."},{"family":"Ali","given":"Hazem I."}],"citation-key":"hadiControlCOVID19System2021a","container-title":"Biomedical Signal Processing and Control","container-title-short":"Biomedical Signal Processing and Control","DOI":"10.1016/j.bspc.2020.102317","ISSN":"1746-8094","issued":{"date-parts":[["2021",2,1]]},"page":"102317","source":"ScienceDirect","title":"Control of COVID-19 system using a novel nonlinear robust control algorithm","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/S1746809420304341","volume":"64"},
  {"id":"hahnAUTOMATEDCYBERSECURITY","abstract":"Nuclear Power Plants (NPPs) are a complex system of coupled physics controlled by a network of Programmable Logic Controllers (PLCs). These PLCs communicate process data across the network to coordinate control actions with each other and inform the operators of process variables and control decisions. Networking the PLCs allows more effective process control and provides the operator more information which results in more efficient plant operation. This interconnectivity creates new security issues, as operators have more access to the plant controls, so will bad actors.","author":[{"family":"Hahn","given":"Andrew"},{"family":"Sandoval","given":"Daniel R"},{"family":"Fasano","given":"Raymond E"},{"family":"Lamb","given":"Christopher"}],"citation-key":"hahnAUTOMATEDCYBERSECURITY","language":"en","source":"Zotero","title":"AUTOMATED CYBER SECURITY TESTING PLATFORM FOR INDUSTRIAL CONTROL SYSTEMS","type":"article-journal"},
  {"id":"hahnSMARTTOT_Emulation_Data_BrokerMain","accessed":{"date-parts":[["2024",8,14]]},"author":[{"family":"Hahn","given":"A S"}],"citation-key":"hahnSMARTTOT_Emulation_Data_BrokerMain","title":"SMARTT/OT_Emulation_Data_Broker at main · sandialabs/SMARTT","type":"webpage","URL":"https://github.com/sandialabs/SMARTT/tree/main/OT_Emulation_Data_Broker"},
  {"id":"hailesellasieIntrusionDetectionPLCBased2018","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Hailesellasie","given":"Muluken"},{"family":"Hasan","given":"Syed Rafay"}],"citation-key":"hailesellasieIntrusionDetectionPLCBased2018","container-title":"Journal of Hardware and Systems Security","container-title-short":"J Hardw Syst Secur","DOI":"10.1007/s41635-017-0017-y","ISSN":"2509-3428, 2509-3436","issue":"1","issued":{"date-parts":[["2018",3]]},"language":"en","page":"1-14","source":"DOI.org (Crossref)","title":"Intrusion Detection in PLC-Based Industrial Control Systems Using Formal Verification Approach in Conjunction with Graphs","type":"article-journal","URL":"http://link.springer.com/10.1007/s41635-017-0017-y","volume":"2"},
+  {"id":"hamiltonjr.RobustControllerDesign1997","abstract":"Presented in this paper is the robust idle speed control of a Ford 4⋅6 L V-8 fuel injected engine. The goal of this investigation is to design a robust feedback controller that maintains the idle speed within a 150 rpm tolerance about 600 rpm despite a 20 Nm step torque disturbance delivered by the power steering pump. The controlled input is the by-pass air valve which is subjected to an output saturation constraint. Issues complicating the controller design include the nonlinear nature of the engine dynamics, the induction-to-power delay of the manifold filling dynamics, and the saturation constraint of the by-pass air valve. An experimental verification of the proposed controller is included. © 1997 by John Wiley & Sons, Ltd.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Hamilton Jr.","given":"G. Kent"},{"family":"Franchek","given":"Matthew A."}],"citation-key":"hamiltonjr.RobustControllerDesign1997","container-title":"International Journal of Robust and Nonlinear Control","DOI":"10.1002/(SICI)1099-1239(199706)7:6<609::AID-RNC294>3.0.CO;2-1","ISSN":"1099-1239","issue":"6","issued":{"date-parts":[["1997"]]},"language":"en","license":"Copyright © 1997 John Wiley & Sons, Ltd.","page":"609-627","source":"Wiley Online Library","title":"Robust Controller Design and Experimental Verification of I.c. Engine Speed Control","type":"article-journal","URL":"https://onlinelibrary.wiley.com/doi/abs/10.1002/%28SICI%291099-1239%28199706%297%3A6%3C609%3A%3AAID-RNC294%3E3.0.CO%3B2-1","volume":"7"},
  {"id":"hancockIncorporationThermalHydraulic2021","abstract":"This report describes the development, modeling, and results of a generic pressurized water reactor power plant simulator that incorporates coupled electrical and thermal power dispatch to an industrial process located approximately one kilometer from the nuclear power plant. The simulator is a commercial PWR simulator that has been modified to include thermal power dispatch as described in past milestone reports [ , ]. The commercial PWR simulator is a generic simulator available from GSE SYSTEMS® (Sykesville, MD, USA) that is built using RELAP5-HDTM Real-Time Solution and in-house software developed by GSE Systems. This generic PWR (GPWR) simulator performs real-time simulation of the complete power plant from the reactor neutronics to the electricity generation and distribution. All primary, secondary, and auxiliary systems are modeled including all control logic in order to provide the most accurate representation of actual nuclear power plant (NPP) operation, and the simulator results have been rigorously verified by an actual NPP operating at approximately 1 GWe. This report is a continuation of worked performed in previous years, and supplemental information from previous reports is included in the appendix for reference.","accessed":{"date-parts":[["2022",3,30]]},"author":[{"family":"Hancock","given":"Stephen G."},{"family":"Westover","given":"Tyler L."},{"family":"Luo","given":"Yusheng"}],"citation-key":"hancockIncorporationThermalHydraulic2021","issued":{"date-parts":[["2021",7,31]]},"language":"English","number":"INL/EXT-21-63226-Rev000","publisher":"Idaho National Lab. (INL), Idaho Falls, ID (United States)","source":"www.osti.gov","title":"Incorporation of Thermal Hydraulic Models for Thermal Power Dispatch into a PWR Power Plant Simulator","type":"report","URL":"https://www.osti.gov/biblio/1835110"},
  {"id":"hanDeepLinkEquating2023","abstract":"Mathematical logic and the code of computer programs are, in an exact way, mirror images of each other.","accessed":{"date-parts":[["2024",1,28]]},"author":[{"family":"Han","given":"Sheon"}],"citation-key":"hanDeepLinkEquating2023","issued":{"date-parts":[["2023",10,11]]},"title":"The Deep Link Equating Math Proofs and Computer Programs","type":"webpage","URL":"https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/"},
  {"id":"harrisonConstructingCloudBasedIDS2012","abstract":"Cloud computing has emerged in recent years as a major segment of the IT industry; however, security concerns remain the primary impediment to full-scale adoption. Leveraging properties of virtualization, virtual machine introspection (VMI) has yielded promising research for cloud security yet adoption of these approaches in production environments remains minimal due to a semantic gap: the extraction of high-level knowledge of the guest operating system's state from low-level artifacts collected out-of-VM. Within the field of forensic memory analysis (FMA), a similar semantic gap exists from the reconstruction of physical memory dumps. We implement a production oriented prototype utilizing designs that combines and narrows these semantic gaps in a modular framework to function as an intrusion detection system (IDS) detecting and defeating post-exploitation activity.","accessed":{"date-parts":[["2023",10,25]]},"author":[{"family":"Harrison","given":"Christopher"},{"family":"Cook","given":"Devin"},{"family":"McGraw","given":"Robert"},{"family":"Hamilton Jr.","given":"John A."}],"citation-key":"harrisonConstructingCloudBasedIDS2012","container-title":"2012 IEEE 11th International Conference on Trust, Security and Privacy in Computing and Communications","DOI":"10.1109/TrustCom.2012.113","event-title":"2012 IEEE 11th International Conference on Trust, Security and Privacy in Computing and Communications","ISSN":"2324-9013","issued":{"date-parts":[["2012",6]]},"page":"163-169","source":"IEEE Xplore","title":"Constructing a Cloud-Based IDS by Merging VMI with FMA","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/6295971?casa_token=QsolkvO1g_AAAAAA:SonsQYxySS_Sn65nJ2R6k1IBzNQXmsqWhnWG6fr47VkZIZaYD6nE6_UxBllmtLP7BEpHbIihP4E"},
@ -460,6 +472,7 @@
  {"id":"kwasinskiModelingCyberPhysicalIntraDependencies2020","abstract":"This paper studies the modeling of cyber-physical dependencies observed within power grids and the effects of these intra-dependencies, on power grid resilience, which is evaluated quantitatively. A fundamental contribution of this paper is the description of the critically important role played by cyber-physical buffers as key components to limit the negative effect of intra-dependencies on power grids resilience. Although resilience issues in the electric power provision service could be limited thanks to the use of local energy storage devices as the realization of service buffers, minimal to no autonomy in data connectivity buffers make cyber vulnerabilities specially critical in terms of resilience. This paper also explains how these models can be used for improved power grids resilience planning considering internal cyber-physical interactions.","author":[{"family":"Kwasinski","given":"Alexis"}],"citation-key":"kwasinskiModelingCyberPhysicalIntraDependencies2020","container-title":"2020 8th Workshop on Modeling and Simulation of Cyber-Physical Energy Systems","DOI":"10.1109/MSCPES49613.2020.9133702","event-title":"2020 8th Workshop on Modeling and Simulation of Cyber-Physical Energy Systems","issued":{"date-parts":[["2020",4]]},"page":"1-6","source":"IEEE Xplore","title":"Modeling of Cyber-Physical Intra-Dependencies in Electric Power Grids and Their Effect on Resilience","type":"paper-conference"},
  {"id":"kwonReachabilityAnalysisSafety2018","accessed":{"date-parts":[["2023",11,3]]},"author":[{"family":"Kwon","given":"Cheolhyeon"},{"family":"Hwang","given":"Inseok"}],"citation-key":"kwonReachabilityAnalysisSafety2018","container-title":"IEEE Transactions on Automatic Control","container-title-short":"IEEE Trans. Automat. Contr.","DOI":"10.1109/TAC.2017.2761762","ISSN":"0018-9286, 1558-2523, 2334-3303","issue":"7","issued":{"date-parts":[["2018",7]]},"page":"2272-2279","source":"DOI.org (Crossref)","title":"Reachability Analysis for Safety Assurance of Cyber-Physical Systems Against Cyber Attacks","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/8063959/","volume":"63"},
  {"id":"kyoung-daekimCyberPhysicalSystems2012","abstract":"Cyber–physical systems (CPSs) are the next generation of engineered systems in which computing, communication, and control technologies are tightly integrated. Research on CPSs is fundamentally important for engineered systems in many important application domains such as transportation, energy, and medical systems. We overview CPS research from both a historical point of view in terms of technologies developed for early generations of control systems, as well as recent results on CPSs in many relevant research domains such as networked control, hybrid systems, real-time computing, real-time networking, wireless sensor networks, security, and model-driven development. We outline the potential for CPSs in many societally important application domains.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"literal":"Kyoung-Dae Kim"},{"family":"Kumar","given":"P. R."}],"citation-key":"kyoung-daekimCyberPhysicalSystems2012","container-title":"Proceedings of the IEEE","container-title-short":"Proc. IEEE","DOI":"10.1109/JPROC.2012.2189792","ISSN":"0018-9219, 1558-2256","issue":"Special Centennial Issue","issued":{"date-parts":[["2012",5]]},"language":"en","page":"1287-1308","source":"DOI.org (Crossref)","title":"Cyber–Physical Systems: A Perspective at the Centennial","title-short":"Cyber–Physical Systems","type":"article-journal","URL":"http://ieeexplore.ieee.org/document/6176187/","volume":"100"},
+  {"id":"lamarshIntroductionNuclearEngineering2018","author":[{"family":"Lamarsh","given":"John R."},{"family":"Baratta","given":"Anthony John"}],"citation-key":"lamarshIntroductionNuclearEngineering2018","edition":"Fourth edition","event-place":"Hoboken","ISBN":"978-0-13-457005-1","issued":{"date-parts":[["2018"]]},"language":"eng","number-of-pages":"802","publisher":"Pearson Education","publisher-place":"Hoboken","source":"K10plus ISBN","title":"Introduction to nuclear engineering","type":"book"},
  {"id":"langFormalVerificationApplied","author":[{"family":"Lang","given":"Kendra"},{"family":"Klett","given":"Corbin"},{"family":"Hawkins","given":"Kelsey"},{"family":"Feron","given":"Eric"},{"family":"Tsiotras","given":"Panagiotis"},{"family":"Phillips","given":"Sean"}],"citation-key":"langFormalVerificationApplied","language":"en","source":"Zotero","title":"Formal Veriﬁcation Applied to Autonomous Spacecraft Attitude Control","type":"article-journal"},
  {"id":"langFormalVerificationApplied2021","abstract":"Formal verification tools are cited as an essential component to enable more widespread development and adoption of advanced autonomous systems. While numerous techniques and tools exist, the applicability of these tools to actual systems under development is currently uncertain. There are myriad reasons for such uncertainty, mostly stemming from assumptions necessary for such tools to work, such as: 1) The assumption that an underlying dynamics model or Simulink model is available, 2) The assumption that the dynamics are low-dimensional, 3) The assumption that the dynamics are linear or linearizable without sacrificing accuracy, and 4) The assumption that the underlying controllers and autonomy algorithms are available and easily modeled. This paper first presents a novel satellite benchmark that incorporates autonomous switching between multiple modes of operation related to attitude control. The result is a hybrid system with nonlinear rotational dynamics restricted to a manifold within each mode. Several open source verification tools are then applied to this benchmark to determine any results that can be drawn about the stability of the overall system. We provide a thorough comparison and discussion of the benefits and drawbacks of those tools we tested, none of which were capable of completely verifying stability requirements over the entire benchmark to the best of our efforts. We also discuss the significant hurdles that remain to implementing these tools on realistic autonomous systems, and the techniques we have found to be the most applicable. The contributions of this paper are: 1) a challenging benchmark on which developers can test their verification tools, and 2) a useful starting point to anyone who wants to apply formal methods to autonomous aerospace systems and to advance the conversation on what remains to be accomplished for these tools to be of practical use.","accessed":{"date-parts":[["2023",11,3]]},"author":[{"family":"Lang","given":"Kendra"},{"family":"Klett","given":"Corbin"},{"family":"Hawkins","given":"Kelsey"},{"family":"Feron","given":"Eric"},{"family":"Tsiotras","given":"Panagiotis"},{"family":"Phillips","given":"Sean"}],"citation-key":"langFormalVerificationApplied2021","container-title":"AIAA Scitech 2021 Forum","DOI":"10.2514/6.2021-1126","ISSN":"9781624106095","issued":{"date-parts":[["2021",1,1]]},"page":"1-14","publisher":"American Institute of Aeronautics and Astronautics Inc, AIAA","source":"KAUST FACULTY PORTAL","title":"Formal verification applied to autonomous spacecraft attitude control","type":"article-journal","URL":"https://arc.aiaa.org/doi/10.2514/6.2021-1126"},
  {"id":"LangleyFormalMethods","citation-key":"LangleyFormalMethods","container-title":"Langley Formal Methods","title":"Langley Formal Methods","type":"webpage","URL":"https://shemesh.larc.nasa.gov/fm/index.html"},
@ -493,6 +506,7 @@
  {"id":"luDetectionIdentificationSparse2023","abstract":"This article investigates the attack detection and identification problem for cyber-physical systems under sparse sensor attacks. A novel candidate set construction algorithm, where only partial combinations of different channels are checked, is proposed to efficiently generate the candidate set containing all the possible sets of corrupted channels under stealthy attacks. Besides, through introducing a unified attack model that precisely characterizes the attack performance and stealthiness, necessary and sufficient conditions for the existence of undetectable/unidentifiable attacks are proposed. Based on the obtained conditions, a novel attack detection and identification strategy is proposed. Compared with the existing methods focusing only on the measurements, more attacks can be detected/identified through introducing side information and the reliability of detector is enhanced through making full use of the attack performance analysis result. Finally, a numerical simulation is provided to illustrate the correctness and effectiveness of the proposed conditions and methods.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Lu","given":"An-Yang"},{"family":"Yang","given":"Guang-Hong"}],"citation-key":"luDetectionIdentificationSparse2023","container-title":"IEEE Transactions on Automatic Control","DOI":"10.1109/TAC.2022.3218545","ISSN":"1558-2523","issue":"9","issued":{"date-parts":[["2023",9]]},"page":"5349-5364","source":"IEEE Xplore","title":"Detection and Identification of Sparse Sensor Attacks in Cyber-Physical Systems With Side Information","type":"article-journal","URL":"https://ieeexplore.ieee.org/abstract/document/9933841?casa_token=GQHa-q6eXQcAAAAA:k-CtF5gsoXIEF9Lo2AQEp-j-9Xr2kaweVGewjVYZk9qyJi21C_roFNSL8HC3AqemtGve_y83LA","volume":"68"},
  {"id":"lundbergConsistentIndividualizedFeature2019","abstract":"Interpreting predictions from tree ensemble methods such as gradient boosting machines and random forests is important, yet feature attribution for trees is often heuristic and not individualized for each prediction. Here we show that popular feature attribution methods are inconsistent, meaning they can lower a feature’s assigned importance when the true impact of that feature actually increases. This is a fundamental problem that casts doubt on any comparison between features. To address it we turn to recent applications of game theory and develop fast exact tree solutions for SHAP (SHapley Additive exPlanation) values, which are the unique consistent and locally accurate attribution values. We then extend SHAP values to interaction effects and define SHAP interaction values. We propose a rich visualization of individualized feature attributions that improves over classic attribution summaries and partial dependence plots, and a unique “supervised” clustering (clustering based on feature attributions). We demonstrate better agreement with human intuition through a user study, exponential improvements in run time, improved clustering performance, and better identification of influential features. An implementation of our algorithm has also been merged into XGBoost and LightGBM, see http://github.com/slundberg/shap for details.","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Lundberg","given":"Scott M."},{"family":"Erion","given":"Gabriel G."},{"family":"Lee","given":"Su-In"}],"citation-key":"lundbergConsistentIndividualizedFeature2019","issued":{"date-parts":[["2019",3,6]]},"language":"en","number":"arXiv:1802.03888","publisher":"arXiv","source":"arXiv.org","title":"Consistent Individualized Feature Attribution for Tree Ensembles","type":"article","URL":"http://arxiv.org/abs/1802.03888"},
  {"id":"lundbergUnifiedApproachInterpreting2017","abstract":"Understanding why a model makes a certain prediction can be as crucial as the prediction’s accuracy in many applications. However, the highest accuracy for large modern datasets is often achieved by complex models that even experts struggle to interpret, such as ensemble or deep learning models, creating a tension between accuracy and interpretability. In response, various methods have recently been proposed to help users interpret the predictions of complex models, but it is often unclear how these methods are related and when one method is preferable over another. To address this problem, we present a uniﬁed framework for interpreting predictions, SHAP (SHapley Additive exPlanations). SHAP assigns each feature an importance value for a particular prediction. Its novel components include: (1) the identiﬁcation of a new class of additive feature importance measures, and (2) theoretical results showing there is a unique solution in this class with a set of desirable properties. The new class uniﬁes six existing methods, notable because several recent methods in the class lack the proposed desirable properties. Based on insights from this uniﬁcation, we present new methods that show improved computational performance and/or better consistency with human intuition than previous approaches.","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Lundberg","given":"Scott"},{"family":"Lee","given":"Su-In"}],"citation-key":"lundbergUnifiedApproachInterpreting2017","issued":{"date-parts":[["2017",11,24]]},"language":"en","number":"arXiv:1705.07874","publisher":"arXiv","source":"arXiv.org","title":"A Unified Approach to Interpreting Model Predictions","type":"article","URL":"http://arxiv.org/abs/1705.07874"},
+  {"id":"lynchDynamicalSystemsApplications2018","abstract":"Dynamical Systems with Applications using Python","author":[{"family":"Lynch","given":"Stephen"}],"citation-key":"lynchDynamicalSystemsApplications2018","DOI":"10.1007/978-3-319-78145-7","edition":"1","event-place":"Cham","ISBN":"978-3-319-78145-7","issued":{"date-parts":[["2018"]]},"language":"eng","publisher":"Springer International Publishing","publisher-place":"Cham","source":"pitt.primo.exlibrisgroup.com","title":"Dynamical Systems with Applications using Python","type":"book"},
  {"id":"maccaroneADVANCEDREACTORCYBER","author":[{"family":"Maccarone","given":"L T"},{"family":"Hahn","given":"A S"},{"family":"Valme","given":"R"},{"family":"Rowland","given":"M T"},{"family":"Kapuria","given":"A"},{"family":"Zhang","given":"Y"},{"family":"Cole","given":"D G"}],"citation-key":"maccaroneADVANCEDREACTORCYBER","language":"en","source":"Zotero","title":"ADVANCED REACTOR CYBER ANALYSIS AND DEVELOPMENT ENVIRONMENT (ARCADE) FOR UNIVERSITY RESEARCH","type":"article-journal"},
  {"id":"mackenzieMechanizingProofComputing2004","author":[{"family":"MacKenzie","given":"Donald"}],"citation-key":"mackenzieMechanizingProofComputing2004","ISBN":"0-262-63295-0","issued":{"date-parts":[["2004"]]},"publisher":"MIT Press","title":"Mechanizing proof: computing, risk, and trust","type":"book"},
  {"id":"madniModelbasedSystemsEngineering2018","abstract":"As systems continue to grow in scale and complexity, the Systems Engineering community has turned to Model-Based Systems Engineering (MBSE) tomanage complexity, maintain consistency, and assure traceability during system development. It is different from \"engineering with models,\" which has been a common practice in the engineering profession for decades. MBSE is a holistic, systems engineering approach centered on the evolving system model, which serves as the \"sole source of truth\" about the system. It comprises system specification, design, validation, and configuration management. Even though MBSE is beginning to see a fair amount of use in multiple industries, specific advances are needed on multiple fronts to realize its full benefits. This paper discusses the motivation for MBSE, and its current state of maturity. It presents systems modeling methodologies and the role of ontologies and metamodels in MBSE. It presents model-based verification and validation (V&V) as an example of MBSE use. An illustrative example of the use of MBSE for design synthesis is presented to demonstrate an important MBSE capability. The paper concludes with a discussion of challenges to widescale adoption and offers promising research directions to fully realize the potential benefits of MBSE.","accessed":{"date-parts":[["2023",10,3]]},"author":[{"family":"Madni","given":"Azad M."},{"family":"Sievers","given":"Michael"}],"citation-key":"madniModelbasedSystemsEngineering2018","container-title":"SYSTEMS ENGINEERING","container-title-short":"Syst. Eng.","DOI":"10.1002/sys.21438","event-place":"Hoboken","ISSN":"1098-1241, 1520-6858","issue":"3","issued":{"date-parts":[["2018",5]]},"language":"English","note":"Web of Science ID: WOS:000435285700004","number-of-pages":"19","page":"172-190","publisher":"Wiley","publisher-place":"Hoboken","source":"Clarivate Analytics Web of Science","title":"Model-based systems engineering: Motivation, current status, and research opportunities","title-short":"Model-based systems engineering","type":"article-journal","URL":"https://www.webofscience.com/wos/woscc/summary/563bee91-8c90-4554-ae8d-46c3ce0028ee-a808dfa0/relevance/1","volume":"21"},
@ -508,6 +522,7 @@
  {"id":"massotWhyFormalizeMathematics","abstract":"We’ve been doing mathematics for more than two thousand years with remarkable success. Hence it is natural to be puzzled by people investing a lot of time and energy into a very new and weird way of doing mathematics: the formalized way where human beings explain mathematical definitions and proofs to computers. Beyond puzzlement, some people are wary. They think the traditional way may disappear, or maybe even mathematicians may disappear, being replaced by AI agents. These events are extremely unlikely and they are not the goals of the mathematical formalization community. We want to add to our tool set, without loosing anything we already have. In this text I’ll explain what we want to add, distinguishing what already partially exists and what is currently science fiction. Examples will use Lean, a proof assistant software developed mostly by Leonardo de Moura at Microsoft Research, but everything I’ll write applies to other proof assistants such as Coq or Isabelle.","author":[{"family":"Massot","given":"Patrick"}],"citation-key":"massotWhyFormalizeMathematics","language":"en","source":"Zotero","title":"Why formalize mathematics?","type":"article-journal"},
  {"id":"MathlibStatistics","accessed":{"date-parts":[["2024",1,28]]},"citation-key":"MathlibStatistics","title":"Mathlib statistics","type":"webpage","URL":"https://leanprover-community.github.io/mathlib_stats.html"},
  {"id":"mattosLatentAutoregressiveGaussian2016","accessed":{"date-parts":[["2022",4,21]]},"author":[{"family":"Mattos","given":"César Lincoln C."},{"family":"Damianou","given":"Andreas"},{"family":"Barreto","given":"Guilherme A."},{"family":"Lawrence","given":"Neil D."}],"citation-key":"mattosLatentAutoregressiveGaussian2016","container-title":"IFAC-PapersOnLine","container-title-short":"IFAC-PapersOnLine","DOI":"10.1016/j.ifacol.2016.07.353","ISSN":"24058963","issue":"7","issued":{"date-parts":[["2016"]]},"language":"en","page":"1121-1126","source":"DOI.org (Crossref)","title":"Latent Autoregressive Gaussian Processes Models for Robust System Identification","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S2405896316305602","volume":"49"},
+  {"id":"matusuRegionsRobustRelative2023","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Matušů","given":"Radek"},{"family":"Senol","given":"Bilal"},{"family":"Pekař","given":"Libor"}],"citation-key":"matusuRegionsRobustRelative2023","container-title":"Heliyon","container-title-short":"Heliyon","DOI":"10.1016/j.heliyon.2023.e18924","ISSN":"2405-8440","issue":"8","issued":{"date-parts":[["2023",8,1]]},"language":"English","PMID":"37560646","publisher":"Elsevier","source":"www.cell.com","title":"Regions of robust relative stability for PI controllers and LTI plants with unstructured multiplicative uncertainty: A second-order-based example","title-short":"Regions of robust relative stability for PI controllers and LTI plants with unstructured multiplicative uncertainty","type":"article-journal","URL":"https://www.cell.com/heliyon/abstract/S2405-8440(23)06132-7","volume":"9"},
  {"id":"mazeikaMBSEsecModelBasedSystems2020","abstract":"This paper presents how Model-Based System Engineering (MBSE) could be leveraged in order to mitigate security risks at an early stage of system development. Primarily, MBSE was used to manage complex engineering projects in terms of system requirements, design, analysis, verification, and validation activities, leaving security aspects aside. However, previous research showed that security requirements and risks could be tackled in the MBSE model, and powerful MBSE tools such as simulation, change impact analysis, automated document generation, validation, and verification could be successfully reused in the multidisciplinary field. This article analyzes various security-related techniques and then clarifies how these techniques can be represented in the Systems Modeling Language (SysML) model and then further exploited with MBSE tools. The paper introduces the MBSEsec method, which gives guidelines for the security analysis process, the SysML/UML-based security profile, and recommendations on what security technique is needed at each security process phase. The MBSEsec method was verified by creating an application case study that reflects real-world problems and running an experiment where systems and security engineers evaluated the feasibility of our approach.","accessed":{"date-parts":[["2023",10,3]]},"author":[{"family":"Mazeika","given":"Donatas"},{"family":"Butleris","given":"Rimantas"}],"citation-key":"mazeikaMBSEsecModelBasedSystems2020","container-title":"APPLIED SCIENCES-BASEL","container-title-short":"Appl. Sci.-Basel","DOI":"10.3390/app10072574","event-place":"Basel","ISSN":"2076-3417","issue":"7","issued":{"date-parts":[["2020",4]]},"language":"English","note":"Web of Science ID: WOS:000533356200373","number-of-pages":"18","page":"2574","publisher":"MDPI","publisher-place":"Basel","source":"Clarivate Analytics Web of Science","title":"MBSEsec: Model-Based Systems Engineering Method for Creating Secure Systems","title-short":"MBSEsec","type":"article-journal","URL":"https://www.webofscience.com/wos/woscc/summary/563bee91-8c90-4554-ae8d-46c3ce0028ee-a808dfa0/relevance/1","volume":"10"},
  {"id":"mclaughlinControllerawareFalseData2014","abstract":"Control systems rely on accurate sensor measurements to safely regulate physical processes. In False Data Injection (FDI) attacks, adversaries inject forged sensor measurements into a control system in hopes of misguiding control algorithms into taking dangerous actions. Traditional FDI attacks mostly require adversaries to know the full system topology, i.e., hundreds or thousands of lines and buses, while having unpredictable consequences. In this paper, we present a new class of FDI attacks directly against individual Programmable Logic Controllers (PLCs), which are ubiquitous in power generation and distribution. Our attack allows the adversary to have only partial information about the victim subsystem, and produces a predictable malicious result. Our attack tool analyzes an I/O trace of the compromised PLCs to produce a set of inputs to achieve the desired PLC outputs, i.e., the system behavior. It proceeds in two steps. First, our tool constructs a model of the PLC's internal logic from the I/O traces. Second, it searches for a set of inputs that cause the model to calculate the desired malicious behavior. We evaluate our tool against a set of representative control systems and show that it is a practical threat against insecure sensor configurations.","accessed":{"date-parts":[["2024",8,8]]},"author":[{"family":"McLaughlin","given":"Stephen"},{"family":"Zonouz","given":"Saman"}],"citation-key":"mclaughlinControllerawareFalseData2014","container-title":"2014 IEEE International Conference on Smart Grid Communications (SmartGridComm)","DOI":"10.1109/SmartGridComm.2014.7007754","event-title":"2014 IEEE International Conference on Smart Grid Communications (SmartGridComm)","issued":{"date-parts":[["2014",11]]},"page":"848-853","source":"IEEE Xplore","title":"Controller-aware false data injection against programmable logic controllers","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/7007754?casa_token=5fHXmr3Mw0gAAAAA:MwJ9mQcpKC7sgnJWqqUnn8wpx4Xs3qWnul5Vmski8Q9Key0ZrsnuqOPyxXKzONdiNpv7Dc_Oews"},
  {"id":"medeirosFaultIntrusionTolerant2011","accessed":{"date-parts":[["2022",3,31]]},"author":[{"family":"Medeiros","given":"Nuno André Carnido"}],"citation-key":"medeirosFaultIntrusionTolerant2011","genre":"Master's thesis","issued":{"date-parts":[["2011"]]},"language":"eng","license":"openAccess","note":"Accepted: 2013-07-16T11:03:46Z","publisher":"University of Lisbon","source":"repositorio.ul.pt","title":"A fault - and intrusion - tolerant architecture for EDP Distribuição SCADA system","type":"thesis","URL":"https://repositorio.ul.pt/handle/10451/8812"},
@ -727,6 +742,7 @@
  {"id":"SEBoK","abstract":"The Guide to the Systems Engineering Body of Knowledge (SEBoK) is a living, authoritative guide of the Systems Engineering discipline.","accessed":{"date-parts":[["2023",10,6]]},"citation-key":"SEBoK","language":"en","title":"SEBoK","type":"webpage","URL":"https://sebokwiki.org/wiki/Guide_to_the_Systems_Engineering_Body_of_Knowledge_(SEBoK)"},
  {"id":"sedjelmaciCyberSecurityBased2020","abstract":"The ten papers in this special issue focus on cybersecurity for cyber-physical systems (CPSs). The systems have become very complex, more sophisticated, intelligent and autonomous. They offer very complex interaction between heterogeneous cyber and physical components; additionally to this complexity, they are exposed to important disturbances due to unintentional and intentional events which make the prediction of their behaviors a very difficult task. Meanwhile, cyber security for CPS is attracting the attention of research scientists in both industry and academia since the number of cyber-attacks have increased and their behaviors have become more sophisticated, commonly known as zero-day threats. the papers in this issue aim to bring together researchers from academic and industry to share their vision of AI application in the cyber security context, and present challenges and recent works and advances related to AI-based cyber security applied to CPSs.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Sedjelmaci","given":"Hichem"},{"family":"Guenab","given":"Fateh"},{"family":"Senouci","given":"Sidi-Mohammed"},{"family":"Moustafa","given":"Hassnaa"},{"family":"Liu","given":"Jiajia"},{"family":"Han","given":"Shuai"}],"citation-key":"sedjelmaciCyberSecurityBased2020","container-title":"IEEE Network","DOI":"10.1109/MNET.2020.9105926","ISSN":"1558-156X","issue":"3","issued":{"date-parts":[["2020",5]]},"page":"6-7","source":"IEEE Xplore","title":"Cyber Security Based on Artificial Intelligence for Cyber-Physical Systems","type":"article-journal","URL":"https://ieeexplore.ieee.org/abstract/document/9105926","volume":"34"},
  {"id":"selvarajuGradCAMVisualExplanations2020","abstract":"We propose a technique for producing ‘visual explanations’ for decisions from a large class of Convolutional Neural Network (CNN)-based models, making them more transparent and explainable.","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Selvaraju","given":"Ramprasaath R."},{"family":"Cogswell","given":"Michael"},{"family":"Das","given":"Abhishek"},{"family":"Vedantam","given":"Ramakrishna"},{"family":"Parikh","given":"Devi"},{"family":"Batra","given":"Dhruv"}],"citation-key":"selvarajuGradCAMVisualExplanations2020","container-title":"International Journal of Computer Vision","container-title-short":"Int J Comput Vis","DOI":"10.1007/s11263-019-01228-7","ISSN":"0920-5691, 1573-1405","issue":"2","issued":{"date-parts":[["2020",2]]},"language":"en","page":"336-359","source":"arXiv.org","title":"Grad-CAM: Visual Explanations from Deep Networks via Gradient-based Localization","title-short":"Grad-CAM","type":"article-journal","URL":"http://arxiv.org/abs/1610.02391","volume":"128"},
+  {"id":"senameRobustControlLinear2013","accessed":{"date-parts":[["2024",10,9]]},"citation-key":"senameRobustControlLinear2013","collection-title":"Lecture Notes in Control and Information Sciences","DOI":"10.1007/978-3-642-36110-4","editor":[{"family":"Sename","given":"Olivier"},{"family":"Gaspar","given":"Peter"},{"family":"Bokor","given":"József"}],"event-place":"Berlin, Heidelberg","ISBN":"978-3-642-36109-8 978-3-642-36110-4","issued":{"date-parts":[["2013"]]},"language":"en","license":"https://www.springernature.com/gp/researchers/text-and-data-mining","publisher":"Springer","publisher-place":"Berlin, Heidelberg","source":"DOI.org (Crossref)","title":"Robust Control and Linear Parameter Varying Approaches: Application to Vehicle Dynamics","title-short":"Robust Control and Linear Parameter Varying Approaches","type":"book","URL":"https://link.springer.com/10.1007/978-3-642-36110-4","volume":"437"},
  {"id":"sguegliaFederalOfficialsInvestigating2023","abstract":"A Pennsylvania water utility is still dealing with the fallout of pro-Iran hackers breaching some of its industrial equipment four days ago, including having to operate one of its water pump stations in manual mode, the utility’s general manager told CNN on Tuesday.","accessed":{"date-parts":[["2024",8,13]]},"author":[{"family":"Sgueglia","given":"Sean Lyngaas","suffix":"By Kristina"}],"citation-key":"sguegliaFederalOfficialsInvestigating2023","container-title":"CNN","issued":{"date-parts":[["2023",11,28]]},"language":"en","title":"Federal officials investigating after pro-Iran group allegedly hacked water authority in Pennsylvania","type":"webpage","URL":"https://www.cnn.com/2023/11/28/us/pennsylvania-water-cyberattack/index.html"},
  {"id":"sharfAssumeGuaranteeContracts2021","abstract":"Modern engineering systems include many components of diﬀerent types and functions. Verifying that these systems satisfy given speciﬁcations can be an arduous task, as most formal veriﬁcation methods are limited to systems of moderate size. Recently, contract theory has been proposed as a modular framework for deﬁning speciﬁcations. In this paper, we present a contract theory for discrete-time dynamical control systems relying on assume/guarantee contracts, which prescribe assumptions on the input of the system and guarantees on the output. We then focus on contracts deﬁned by linear constraints, and develop eﬃcient computational tools for veriﬁcation of satisfaction and reﬁnement based on linear programming. We exemplify these tools in a simulation example, proving a certain safety speciﬁcation for a two-vehicle autonomous driving setting.","accessed":{"date-parts":[["2023",11,8]]},"author":[{"family":"Sharf","given":"Miel"},{"family":"Besselink","given":"Bart"},{"family":"Molin","given":"Adam"},{"family":"Zhao","given":"Qiming"},{"family":"Johansson","given":"Karl Henrik"}],"citation-key":"sharfAssumeGuaranteeContracts2021","issued":{"date-parts":[["2021",4,19]]},"language":"en","number":"arXiv:2012.12657","publisher":"arXiv","source":"arXiv.org","title":"Assume/Guarantee Contracts for Dynamical Systems: Theory and Computational Tools","title-short":"Assume/Guarantee Contracts for Dynamical Systems","type":"article","URL":"http://arxiv.org/abs/2012.12657"},
  {"id":"shevitzLyapunovStabilityTheory1994","accessed":{"date-parts":[["2024",3,4]]},"author":[{"family":"Shevitz","given":"D."},{"family":"Paden","given":"B."}],"citation-key":"shevitzLyapunovStabilityTheory1994","container-title":"IEEE Transactions on Automatic Control","container-title-short":"IEEE Trans. Automat. Contr.","DOI":"10.1109/9.317122","ISSN":"00189286","issue":"9","issued":{"literal":"Sept./1994"},"page":"1910-1914","source":"DOI.org (Crossref)","title":"Lyapunov stability theory of nonsmooth systems","type":"article-journal","URL":"http://ieeexplore.ieee.org/document/317122/","volume":"39"},
@ -773,6 +789,8 @@
  {"id":"srivastavaDigitalTwinsServing2024a","abstract":"Today’s critical infrastructure systems are more interconnected and dependent on the electric power grid. This interdependence means that disruptions in one system can have far-reaching consequences across many others. This is particularly evident when a cyberattack in the power grid leads to widespread outages and disrupts essential societal services. To prevent such disasters, it is crucial that proactive actions are taken to secure our power grid control centers and digital substations. This is where digital twins (DTs) play an important role: By creating virtual replicas of cyberphysical assets and processes, DTs allow system operators to anticipate and address potential vulnerabilities in our cybersecurity defenses before they can be exploited. As such, a DT can be considered as a key contributor to safeguard the power system against cyberattacks. This article examines the potential future benefits of DTs in enabling a cybersecure and resilient power grid, explores multiple use cases, and proposes a path forward.","accessed":{"date-parts":[["2024",3,13]]},"author":[{"family":"Srivastava","given":"Anurag"},{"family":"Liu","given":"Chen-Ching"},{"family":"Stefanov","given":"Alexandru"},{"family":"Basumallik","given":"Sagnik"},{"family":"Hussain","given":"Mohammed M."},{"family":"Somda","given":"Baza"},{"family":"Rajkumar","given":"Vetrivel S."}],"citation-key":"srivastavaDigitalTwinsServing2024a","container-title":"IEEE Power and Energy Magazine","DOI":"10.1109/MPE.2023.3325196","ISSN":"1558-4216","issue":"1","issued":{"date-parts":[["2024",1]]},"page":"61-71","source":"IEEE Xplore","title":"Digital Twins Serving Cybersecurity: More Than a Model: Cybersecurity as a Future Benefit of Digital Twins 2","title-short":"Digital Twins Serving Cybersecurity","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/10398550/","volume":"22"},
  {"id":"STALIROTALIROTOOLS","abstract":"TALIRO (TemporAl LogIC RObustness) tools is a suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics.","accessed":{"date-parts":[["2023",10,13]]},"citation-key":"STALIROTALIROTOOLS","title":"S-TALIRO - TALIRO-TOOLS","type":"webpage","URL":"https://sites.google.com/a/asu.edu/s-taliro/s-taliro"},
  {"id":"standalone","abstract":"The standalone bundle allows users to easily place picture environments or other material in own source ﬁles and compile these on their own or as part of a main document. A special standalone class is provided for use with such ﬁles, which by default crops the resulting output ﬁle to the content. The standalone package enables the user to simply load the standalone ﬁles using \\input inside a main document.","author":[{"family":"Scharrer","given":"Martin"}],"citation-key":"standalone","language":"en","page":"29","source":"Zotero","title":"standalone Package","type":"article-journal"},
+  {"id":"stevebruntonControlBootcampCautionary2017","abstract":"Here we show an example of why it can be a very bad idea to invert some plant dynamics, for example with unstable eigenvalues, for loop shaping.  \n\nCode available at: faculty.washington.edu/sbrunton/control_bootcamp_code.zip\n\nThese lectures follow Chapters 1 & 3 from:\n\nMachine learning control, by Duriez, Brunton, & Noack\nhttps://www.amazon.com/Machine-Learni...\n\nChapters available at: http://faculty.washington.edu/sbrunto...\n\nThis video was produced at the University of Washington","accessed":{"date-parts":[["2024",10,9]]},"citation-key":"stevebruntonControlBootcampCautionary2017","dimensions":"5:18","director":[{"literal":"Steve Brunton"}],"issued":{"date-parts":[["2017",3,8]]},"source":"YouTube","title":"Control Bootcamp:  Cautionary Tale About Inverting the Plant Dynamics","title-short":"Control Bootcamp","type":"motion_picture","URL":"https://www.youtube.com/watch?v=G9apWx4iaks"},
+  {"id":"stevebruntonControlBootcampIntroduction2017","abstract":"This video motivates robust control with the famous 1978 paper by John Doyle, titled \"Guaranteed Margins for LQG Regulators\"... Abstract:  There are none.  \n\nCode available at: faculty.washington.edu/sbrunton/control_bootcamp_code.zip\n\nThese lectures follow Chapters 1 & 3 from:\n\nMachine learning control, by Duriez, Brunton, & Noack\nhttps://www.amazon.com/Machine-Learni...\n\nChapters available at: http://faculty.washington.edu/sbrunto...\n\nThis video was produced at the University of Washington","accessed":{"date-parts":[["2024",10,9]]},"citation-key":"stevebruntonControlBootcampIntroduction2017","dimensions":"8:12","director":[{"literal":"Steve Brunton"}],"issued":{"date-parts":[["2017",3,7]]},"source":"YouTube","title":"Control Bootcamp:  Introduction to Robust Control","title-short":"Control Bootcamp","type":"motion_picture","URL":"https://www.youtube.com/watch?v=Y6MRgg_TGy0"},
  {"id":"stiasnyPhysicsInformedNeuralNetworks2023","abstract":"The simulation of power system dynamics poses a computationally expensive task. Considering the growing uncertainty of generation and demand patterns, thousands of scenarios need to be continuously assessed to ensure the safety of power systems. Physics-Informed Neural Networks (PINNs) have recently emerged as a promising solution for drastically accelerating computations of non-linear dynamical systems. This work investigates the applicability of these methods for power system dynamics, focusing on the dynamic response to load disturbances. Comparing the prediction of PINNs to the solution of conventional solvers, we find that PINNs can be 10 to 1000 times faster than conventional solvers. At the same time, we find them to be sufficiently accurate and numerically stable even for large time steps. To facilitate a deeper understanding, this paper also present a new regularisation of Neural Network (NN) training by introducing a gradient-based term in the loss function. The resulting NNs, which we call dtNNs, help us deliver a comprehensive analysis about the strengths and weaknesses of the NN based approaches, how incorporating knowledge of the underlying physics affects NN performance, and how this compares with conventional solvers for power system dynamics.","accessed":{"date-parts":[["2024",1,30]]},"author":[{"family":"Stiasny","given":"Jochen"},{"family":"Chatzivasileiadis","given":"Spyros"}],"citation-key":"stiasnyPhysicsInformedNeuralNetworks2023","container-title":"Electric Power Systems Research","container-title-short":"Electric Power Systems Research","DOI":"10.1016/j.epsr.2023.109748","ISSN":"03787796","issued":{"date-parts":[["2023",11]]},"page":"109748","source":"arXiv.org","title":"Physics-Informed Neural Networks for Time-Domain Simulations: Accuracy, Computational Cost, and Flexibility","title-short":"Physics-Informed Neural Networks for Time-Domain Simulations","type":"article-journal","URL":"http://arxiv.org/abs/2303.08994","volume":"224"},
  {"id":"stiasnyTransientStabilityAnalysis2023","abstract":"We explore the possibility to use physics-informed neural networks to drastically accelerate the solution of ordinary differential-algebraic equations that govern the power system dynamics. When it comes to transient stability assessment, the traditionally applied methods either carry a significant computational burden, require model simplifications, or use overly conservative surrogate models. Conventional neural networks can circumvent these limitations but are faced with high demand of high-quality training datasets, while they ignore the underlying governing equations. Physics-informed neural networks are different: they incorporate the power system differential algebraic equations directly into the neural network training and drastically reduce the need for training data. This paper takes a deep dive into the performance of physics-informed neural networks for power system transient stability assessment. Introducing a new neural network training procedure to facilitate a thorough comparison, we explore how physics-informed neural networks compare with conventional differential-algebraic solvers and classical neural networks in terms of computation time, requirements in data, and prediction accuracy. We illustrate the findings on the Kundur two-area system, and assess the opportunities and challenges of physics-informed neural networks to serve as a transient stability analysis tool, highlighting possible pathways to further develop this method.","accessed":{"date-parts":[["2024",1,30]]},"author":[{"family":"Stiasny","given":"Jochen"},{"family":"Misyris","given":"Georgios S."},{"family":"Chatzivasileiadis","given":"Spyros"}],"citation-key":"stiasnyTransientStabilityAnalysis2023","issued":{"date-parts":[["2023",3,15]]},"number":"arXiv:2106.13638","publisher":"arXiv","source":"arXiv.org","title":"Transient Stability Analysis with Physics-Informed Neural Networks","type":"article","URL":"http://arxiv.org/abs/2106.13638"},
  {"id":"stoufferGuideIndustrialControl2015","abstract":"This document provides guidance on how to secure Industrial Control Systems (ICS), including Supervisory Control and Data Acquisition (SCADA) systems, Distributed Control Systems (DCS), and other control system configurations such as Programmable Logic Controllers (PLC), while addressing their unique performance, reliability, and safety requirements. The document provides an overview of ICS and typical system topologies, identifies typical threats and vulnerabilities to these systems, and provides recommended security countermeasures to mitigate the associated risks.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Stouffer","given":"Keith"},{"family":"Lightman","given":"Suzanne"},{"family":"Pillitteri","given":"Victoria"},{"family":"Abrams","given":"Marshall"},{"family":"Hahn","given":"Adam"}],"citation-key":"stoufferGuideIndustrialControl2015","DOI":"10.6028/NIST.SP.800-82r2","issued":{"date-parts":[["2015",6,3]]},"language":"en","number":"NIST Special Publication (SP) 800-82 Rev. 2","publisher":"National Institute of Standards and Technology","source":"csrc.nist.gov","title":"Guide to Industrial Control Systems (ICS) Security","type":"report","URL":"https://csrc.nist.gov/pubs/sp/800/82/r2/final"},
@ -792,6 +810,7 @@
  {"id":"szekeresSoKEternalWar2013","abstract":"Memory corruption bugs in software written in low-level languages like C or C++ are one of the oldest problems in computer security. The lack of safety in these languages allows attackers to alter the program's behavior or take full control over it by hijacking its control flow. This problem has existed for more than 30 years and a vast number of potential solutions have been proposed, yet memory corruption attacks continue to pose a serious threat. Real world exploits show that all currently deployed protections can be defeated. This paper sheds light on the primary reasons for this by describing attacks that succeed on today's systems. We systematize the current knowledge about various protection techniques by setting up a general model for memory corruption attacks. Using this model we show what policies can stop which attacks. The model identifies weaknesses of currently deployed techniques, as well as other proposed protections enforcing stricter policies. We analyze the reasons why protection mechanisms implementing stricter polices are not deployed. To achieve wide adoption, protection mechanisms must support a multitude of features and must satisfy a host of requirements. Especially important is performance, as experience shows that only solutions whose overhead is in reasonable bounds get deployed. A comparison of different enforceable policies helps designers of new protection mechanisms in finding the balance between effectiveness (security) and efficiency. We identify some open research problems, and provide suggestions on improving the adoption of newer techniques.","accessed":{"date-parts":[["2023",10,3]]},"author":[{"family":"Szekeres","given":"László"},{"family":"Payer","given":"Mathias"},{"family":"Wei","given":"Tao"},{"family":"Song","given":"Dawn"}],"citation-key":"szekeresSoKEternalWar2013","container-title":"2013 IEEE Symposium on Security and Privacy","DOI":"10.1109/SP.2013.13","event-title":"2013 IEEE Symposium on Security and Privacy","ISSN":"1081-6011","issued":{"date-parts":[["2013",5]]},"page":"48-62","source":"IEEE Xplore","title":"SoK: Eternal War in Memory","title-short":"SoK","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/6547101?casa_token=BS-5MJ0vLmIAAAAA:zbQEgMfdsqfRXpxxi0C6R7go0gaaCAcHsF9WLHt91MdiFDWvo4NS8Xbh7fDNJh44ZI-IarctggU"},
  {"id":"sztipanovitsDesignToolChain2015","abstract":"Design automation tools evolved to support the principle of \"separation of concerns\" to manage engineering complexity. Accordingly, we find tool suites that are vertically integrated with limited support (even intention) for horizontal integratability (i.e. integration across disciplinary boundaries). CPS challenges these established boundaries and with this - market conditions. The question is how to facilitate reorganization and create the foundation and technologies for composable CPS design tool chains that enables reuse of existing commercial and open source tools? In this paper we describe some of the lessons learned in the design and implementation of a design automation tool suite for complex cyber-physical systems (CPS) in the vehicle domain. The tool suite followed a model- and component-based design approach to match the significant increase in design productivity experienced in several narrowly focused homogeneous domains, such as signal processing, control and aspects of electronic design. The primary challenge in the undertaking was the tremendous heterogeneity of complex cyber-physical systems (CPS), where such as vehicles has not yet been achieved. This paper describes some of the challenges addressed and solution approaches to building a comprehensive design tool suite for complex CPS.","accessed":{"date-parts":[["2023",11,8]]},"author":[{"family":"Sztipanovits","given":"Janos"},{"family":"Bapty","given":"Ted"},{"family":"Neema","given":"Sandeep"},{"family":"Koutsoukos","given":"Xenofon"},{"family":"Jackson","given":"Ethan"}],"citation-key":"sztipanovitsDesignToolChain2015","container-title":"Proceedings of the 52nd Annual Design Automation Conference","DOI":"10.1145/2744769.2747922","event-place":"San Francisco California","event-title":"DAC '15: The 52nd Annual Design Automation Conference 2015","ISBN":"978-1-4503-3520-1","issued":{"date-parts":[["2015",6,7]]},"language":"en","page":"1-6","publisher":"ACM","publisher-place":"San Francisco California","source":"DOI.org (Crossref)","title":"Design tool chain for cyber-physical systems: lessons learned","title-short":"Design tool chain for cyber-physical systems","type":"paper-conference","URL":"https://dl.acm.org/doi/10.1145/2744769.2747922"},
  {"id":"tables-tips","author":[{"family":"Robson","given":"Adrian P"}],"citation-key":"tables-tips","language":"en","page":"16","source":"Zotero","title":"LaTeX Table Hints and Tips","type":"article-journal"},
+  {"id":"taghiradRobustPerformanceVerification2008","abstract":"An adaptive robust controller (ARC) has been recently developed for read/write head embedded control systems of hard disk drives (HDDs). This structure is applicable to both track seeking and track following modes, and it makes the mode switching control algorithms found in conventional HDD servosystems unnecessary. An Improved Desired Compensation ARC (IDCARC) scheme is proposed in this paper, in which the traditional ARC is powered by a dynamic adaptive term. In this approach the adaptation regressor is calculated using reference trajectory information. Moreover, a robust analysis of this method is developed, in which a controller designed based on a simple model of the system is verified in a closed loop performance of a more comprehensive model of the system. The simulation result verifies the significant improvement of the performance of IDCARC compared to that of ARC and its robustness for this model. It is observed that in the presence of large disturbances the proposed method preserves the stability and a suitable performance while the ARC fails even in stability.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Taghirad","given":"Hamid D."},{"family":"Jamei","given":"Ehsan"}],"citation-key":"taghiradRobustPerformanceVerification2008","container-title":"IEEE Transactions on Industrial Electronics","DOI":"10.1109/TIE.2007.896502","ISSN":"1557-9948","issue":"1","issued":{"date-parts":[["2008",1]]},"page":"448-456","source":"IEEE Xplore","title":"Robust Performance Verification of Adaptive Robust Controller for Hard Disk Drives","type":"article-journal","URL":"https://ieeexplore.ieee.org/abstract/document/4401189?casa_token=7Jkf_TOKTCkAAAAA:04affOUjExgKv1F-v9iTOGA59YsLtjbaxbkwzudJDa-OlON2ihhn4Eju7MfG4JRgeFKfihmLLw","volume":"55"},
  {"id":"TALIROTOOLS","abstract":"TALIRO (TemporAl LogIC RObustness) tools is a suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics.","accessed":{"date-parts":[["2023",10,13]]},"citation-key":"TALIROTOOLS","title":"TALIRO-TOOLS","type":"webpage","URL":"https://sites.google.com/a/asu.edu/s-taliro/"},
  {"id":"tangeSystematicSurveyIndustrial2020","abstract":"A key application of the Internet of Things (IoT) paradigm lies within industrial contexts. Indeed, the emerging Industrial Internet of Things (IIoT), commonly referred to as Industry 4.0, promises to revolutionize production and manufacturing through the use of large numbers of networked embedded sensing devices, and the combination of emerging computing technologies, such as Fog/Cloud Computing and Artiﬁcial Intelligence. The IIoT is characterized by an increased degree of inter-connectivity, which not only creates opportunities for the industries that adopt it, but also for cyber-criminals. Indeed, IoT security currently represents one of the major obstacles that prevent the widespread adoption of IIoT technology. Unsurprisingly, such concerns led to an exponential growth of published research over the last few years. To get an overview of the ﬁeld, we deem it important to systematically survey the academic literature so far, and distill from it various security requirements as well as their popularity. This paper consists of two contributions: our primary contribution is a systematic review of the literature over the period 2011-2019 on IIoT Security, focusing in particular on the security requirements of the IIoT. Our secondary contribution is a reﬂection on how the relatively new paradigm of Fog computing can be leveraged to address these requirements, and thus improve the security of the IIoT.","accessed":{"date-parts":[["2022",9,30]]},"author":[{"family":"Tange","given":"Koen"},{"family":"De Donno","given":"Michele"},{"family":"Fafoutis","given":"Xenofon"},{"family":"Dragoni","given":"Nicola"}],"citation-key":"tangeSystematicSurveyIndustrial2020","container-title":"IEEE Communications Surveys & Tutorials","container-title-short":"IEEE Commun. Surv. Tutorials","DOI":"10.1109/COMST.2020.3011208","ISSN":"1553-877X, 2373-745X","issue":"4","issued":{"season":4,"date-parts":[[2020]]},"language":"en","page":"2489-2520","source":"DOI.org (Crossref)","title":"A Systematic Survey of Industrial Internet of Things Security: Requirements and Fog Computing Opportunities","title-short":"A Systematic Survey of Industrial Internet of Things Security","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/9146364/","volume":"22"},
  {"id":"taoDigitalTwinIndustry2019","abstract":"Digital twin (DT) is one of the most promising enabling technologies for realizing smart manufacturing and Industry 4.0. DTs are characterized by the seamless integration between the cyber and physical spaces. The importance of DTs is increasingly recognized by both academia and industry. It has been almost 15 years since the concept of the DT was initially proposed. To date, many DT applications have been successfully implemented in different industries, including product design, production, prognostics and health management, and some other fields. However, at present, no paper has focused on the review of DT applications in industry. In an effort to understand the development and application of DTs in industry, this paper thoroughly reviews the state-of-the-art of the DT research concerning the key components of DTs, the current development of DTs, and the major DT applications in industry. This paper also outlines the current challenges and some possible directions for future work.","accessed":{"date-parts":[["2022",3,8]]},"author":[{"family":"Tao","given":"Fei"},{"family":"Zhan","given":"He"},{"family":"Liu","given":"Ang"},{"family":"Nee","given":"A. Y. C."}],"citation-key":"taoDigitalTwinIndustry2019","container-title":"Ieee Transactions on Industrial Informatics","container-title-short":"IEEE Trans. Ind. Inform.","DOI":"10.1109/TII.2018.2873186","event-place":"Piscataway","ISSN":"1551-3203","issue":"4","issued":{"date-parts":[["2019",4]]},"language":"English","note":"WOS:000467095500054","page":"2405-2415","publisher":"Ieee-Inst Electrical Electronics Engineers Inc","publisher-place":"Piscataway","source":"Web of Science Nextgen","title":"Digital Twin in Industry: State-of-the-Art","title-short":"Digital Twin in Industry","type":"article-journal","URL":"http://www.webofscience.com/wos/woscc/summary/marked/relevance/1","volume":"15"},
@ -849,6 +868,7 @@
  {"id":"wangFormalAnalysisSecurity2017","abstract":"For the research and development of CyberPhysical System (CPS), the security problems have gradually emerged. This paper explores the design of security for CPS. We focus on a kind of common attacks that destroys the critical system parameters to paralyze the system. Timed Automata are used for formalizing the behaviors of CPS, since the requirements on time are necessary for CPS. The modeling of CPS includes three aspects: the interactions between the various components of the CPS, the attacker, and the recovery mechanism. A modeling framework is given to illustrate our method. We also take the network water level control system as an example to illustrate our modeling processes. By using the model checking tool PAT, the security properties are verified and the results are analyzed.","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Wang","given":"Ting"},{"family":"Su","given":"Qi"},{"family":"Chen","given":"Tieming"}],"citation-key":"wangFormalAnalysisSecurity2017","container-title":"2017 IEEE Second International Conference on Data Science in Cyberspace (DSC)","DOI":"10.1109/DSC.2017.44","event-place":"Shenzhen, China","event-title":"2017 IEEE Second International Conference on Data Science in Cyberspace (DSC)","ISBN":"978-1-5386-1600-0","issued":{"date-parts":[["2017",6]]},"language":"en","page":"534-540","publisher":"IEEE","publisher-place":"Shenzhen, China","source":"DOI.org (Crossref)","title":"Formal Analysis of Security Properties of Cyber-Physical System Based on Timed Automata","type":"paper-conference","URL":"http://ieeexplore.ieee.org/document/8005528/"},
  {"id":"wangFormalModelBasedDesign2019","abstract":"The model-based approach has been widely applied to the design of software. However, most of these approaches depend on simulation and manual code implementation, which reduces the efﬁciency and quality of software. In this paper, we present a new model-based approach, which automatically generates the executable C++ code running on the popular Robot Operation System (ROS). Our approach consists of three phases: modeling, veriﬁcation, and automatic code generation. In the modeling phase, the internal interaction behaviors of robot systems are modeled as a network of timed automata. In the veriﬁcation phase, the safety requirements are formalized and veriﬁed. In the code generation phase, a code generation tool can generate executable C++ code from the veriﬁed timed automata model. It bridges the gap between the formal model and the error-prone system implementation. Compared with existing method, the code generator provides the abstractions and mapping of ROS instructions, which realize the seamless connection between the generated code and ROS. The tool also supports most of the complex structures and advanced features of timed automata such as timer, committed location, and synchronous action. For evaluation, a real-industrial robot application of grasping a cup is conducted using our modelbased design method, and the generated code can be directly deployed and successfully accomplishes the grasping task.","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Wang","given":"Rui"},{"family":"Guan","given":"Yong"},{"family":"Song","given":"Houbing"},{"family":"Li","given":"Xinxin"},{"family":"Li","given":"Xiaojuan"},{"family":"Shi","given":"Zhiping"},{"family":"Song","given":"Xiaoyu"}],"citation-key":"wangFormalModelBasedDesign2019","container-title":"IEEE Systems Journal","container-title-short":"IEEE Systems Journal","DOI":"10.1109/JSYST.2018.2867285","ISSN":"1932-8184, 1937-9234, 2373-7816","issue":"1","issued":{"date-parts":[["2019",3]]},"language":"en","page":"1096-1107","source":"DOI.org (Crossref)","title":"A Formal Model-Based Design Method for Robotic Systems","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/8464674/","volume":"13"},
  {"id":"wangPINNsBasedUncertaintyQuantification2023","abstract":"This paper addresses the challenge of transient stability in power systems with missing parameters and uncertainty propagation in swing equations. We introduce a novel application of Physics-Informed Neural Networks (PINNs), specifically an Ensemble of PINNs (E-PINNs), to estimate critical parameters like rotor angle and inertia coefficient with enhanced accuracy and reduced computational load. E-PINNs capitalize on the underlying physical principles of swing equations to provide a robust solution. Our approach not only facilitates efficient parameter estimation but also quantifies uncertainties, delivering probabilistic insights into the system behavior. The efficacy of E-PINNs is demonstrated through the analysis of $1$-bus and $2$-bus systems, highlighting the model's ability to handle parameter variability and data scarcity. The study advances the application of machine learning in power system stability, paving the way for reliable and computationally efficient transient stability analysis.","accessed":{"date-parts":[["2024",1,30]]},"author":[{"family":"Wang","given":"Ren"},{"family":"Zhong","given":"Ming"},{"family":"Xu","given":"Kaidi"},{"family":"Sánchez-Cortés","given":"Lola Giráldez"},{"family":"Guerra","given":"Ignacio de Cominges"}],"citation-key":"wangPINNsBasedUncertaintyQuantification2023","issued":{"date-parts":[["2023",11,21]]},"number":"arXiv:2311.12947","publisher":"arXiv","source":"arXiv.org","title":"PINNs-Based Uncertainty Quantification for Transient Stability Analysis","type":"article","URL":"http://arxiv.org/abs/2311.12947"},
+  {"id":"wangRobustControlStructural2004","abstract":"Natural hazards, such as earthquakes and strong wind events, place large forces on\ntall, slender structures and on long-span bridges. In view of the numerous uncertainties\ndue to model errors, stress calculations, material properties, and environmental ...","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Wang","given":"Sheng-Guo"},{"family":"Roschke","given":"Paul N."},{"family":"Yeh","given":"H. Y."}],"citation-key":"wangRobustControlStructural2004","container-title":"Journal of Engineering Mechanics","DOI":"10.1061/(ASCE)0733-9399(2004)130:3(337)","ISSN":"0733-9399","issue":"3","issued":{"date-parts":[["2004",3,1]]},"language":"EN","license":"Copyright © 2004 American Society of Civil Engineers","page":"337-346","publisher":"American Society of Civil Engineers","source":"ASCE","title":"Robust Control for Structural Systems with Unstructured Uncertainties","type":"article-journal","URL":"https://ascelibrary.org/doi/10.1061/%28ASCE%290733-9399%282004%29130%3A3%28337%29","volume":"130"},
  {"id":"wankhadeCyberPhysicalSystem2020","abstract":"The next generation of engineered systems is specified as the cyber-physical systems (CPS) with the incorporation of communiqué, computation, and controller to achieve the targets of constancy, routine, sturdiness, and competence in physical systems. Cyber-Physical systems are a feedback system that requires cybersecurity and improved design tools that enables design methodology. Cyber-Physical system becomes a significant track intended for the advance of the smart engineering business. The control trial of wide-ranging and organically disseminated cyber-physical systems is intended to be sturdy and consistent with very multifaceted disseminated in addition to the vital controller. The safety difficulties in addition protective measures the aforementioned aspects are progressively advancing the concentration of exploration in the arena. This paper presents a study of different application framework that is helpful to industry and academia in the direction of design a strong security framework to improve these systems.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Wankhade","given":"Megha"},{"family":"Kottur","given":"Suhasini Vijaykumar"}],"citation-key":"wankhadeCyberPhysicalSystem2020","container-title":"2020 Fourth International Conference on Inventive Systems and Control (ICISC)","DOI":"10.1109/ICISC47916.2020.9171074","event-title":"2020 Fourth International Conference on Inventive Systems and Control (ICISC)","issued":{"date-parts":[["2020",1]]},"page":"716-719","source":"IEEE Xplore","title":"Cyber Physical System Framework: An Apropos Study","title-short":"Cyber Physical System Framework","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/9171074?casa_token=ThzOr3xT16gAAAAA:NktWFIimmo9FAbCfwaYlLywtCc_wYOE0B2TuTlV-stWns1HSOxoQWqD5IlOFQ2FwK4jQ-MJbig"},
  {"id":"WaPo-water","author":[{"family":"Montgomery","given":"Mark"},{"family":"Ravich","given":"Samantha F."}],"citation-key":"WaPo-water","container-title":"The Washington Post","issued":{"literal":"date accesssed 02/13/2022"},"title":"The cybersecurity risk to our water supply is real. We need to prepare","type":"article-journal","URL":"https://www.washingtonpost.com/opinions/2022/01/03/cybersecurity-risk-water-supply/"},
  {"id":"wardellMethodRevealingAddressing2016","abstract":"Several cyber-attacks on the cyber-physical systems (CPS) that monitor and control critical infrastructure were publically announced over the last few years. Almost without exception, the proposed security solutions focus on preventing unauthorized access to the industrial control systems (ICS) at various levels – the defense in depth approach. While useful, it does not address the problem of making the systems more capable of responding to the malicious actions of an attacker once they have gained access to the system. The first step in making an ICS more resilient to an attacker is identifying the cyber security vulnerabilities the attacker can use during system design. This paper presents a method that reveals cyber security vulnerabilities in ICS through the formal modeling of the system and malicious agents. The inclusion of the malicious agent in the analysis of an existing systems identifies security vulnerabilities that are missed in traditional functional model checking.","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Wardell","given":"Dean C."},{"family":"Mills","given":"Robert F."},{"family":"Peterson","given":"Gilbert L."},{"family":"Oxley","given":"Mark E."}],"citation-key":"wardellMethodRevealingAddressing2016","container-title":"Procedia Computer Science","container-title-short":"Procedia Computer Science","DOI":"10.1016/j.procs.2016.09.289","ISSN":"18770509","issued":{"date-parts":[["2016"]]},"language":"en","page":"24-31","source":"DOI.org (Crossref)","title":"A Method for Revealing and Addressing Security Vulnerabilities in Cyber-physical Systems by Modeling Malicious Agent Interactions with Formal Verification","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S1877050916324619","volume":"95"},
@ -871,6 +891,7 @@
  {"id":"xuSurveyIndustrialInternet2018","abstract":"The vision of Industry 4.0, otherwise known as the fourth industrial revolution, is the integration of massively deployed smart computing and network technologies in industrial production and manufacturing settings for the purposes of automation, reliability, and control, implicating the development of an Industrial Internet of Things (I-IoT). Speciﬁcally, I-IoT is devoted to adopting the IoT to enable the interconnection of anything, anywhere, and at any time in the manufacturing system context to improve the productivity, efﬁciency, safety, and intelligence. As an emerging technology, I-IoT has distinct properties and requirements that distinguish it from consumer IoT, including the unique types of smart devices incorporated, network technologies and quality-of-service requirements, and strict needs of command and control. To more clearly understand the complexities of I-IoT and its distinct needs and to present a uniﬁed assessment of the technology from a systems’ perspective, in this paper, we comprehensively survey the body of existing research on I-IoT. Particularly, we ﬁrst present the I-IoT architecture, I-IoT applications (i.e., factory automation and process automation), and their characteristics. We then consider existing research efforts from the three key system aspects of control, networking, and computing. Regarding control, we ﬁrst categorize industrial control systems and then present recent and relevant research efforts. Next, considering networking, we propose a three-dimensional framework to explore the existing research space and investigate the adoption of some representative networking technologies, including 5G, machine-tomachine communication, and software-deﬁned networking. Similarly, concerning computing, we again propose a second three-dimensional framework that explores the problem space of computing in I-IoT and investigate the cloud, edge, and hybrid cloud and edge computing platforms. Finally, we outline particular challenges and future research needs in control, networking, and computing systems, as well as for the adoption of machine learning in an I-IoT context.","accessed":{"date-parts":[["2022",9,30]]},"author":[{"family":"Xu","given":"Hansong"},{"family":"Yu","given":"Wei"},{"family":"Griffith","given":"David"},{"family":"Golmie","given":"Nada"}],"citation-key":"xuSurveyIndustrialInternet2018","container-title":"IEEE Access","container-title-short":"IEEE Access","DOI":"10.1109/ACCESS.2018.2884906","ISSN":"2169-3536","issued":{"date-parts":[["2018"]]},"language":"en","page":"78238-78259","source":"DOI.org (Crossref)","title":"A Survey on Industrial Internet of Things: A Cyber-Physical Systems Perspective","title-short":"A Survey on Industrial Internet of Things","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/8558534/","volume":"6"},
  {"id":"yaacoubCyberphysicalSystemsSecurity2020","accessed":{"date-parts":[["2023",10,11]]},"author":[{"family":"Yaacoub","given":"Jean-Paul A."},{"family":"Salman","given":"Ola"},{"family":"Noura","given":"Hassan N."},{"family":"Kaaniche","given":"Nesrine"},{"family":"Chehab","given":"Ali"},{"family":"Malli","given":"Mohamad"}],"citation-key":"yaacoubCyberphysicalSystemsSecurity2020","container-title":"Microprocessors and Microsystems","container-title-short":"Microprocessors and Microsystems","DOI":"10.1016/j.micpro.2020.103201","ISSN":"01419331","issued":{"date-parts":[["2020",9]]},"language":"en","page":"103201","source":"DOI.org (Crossref)","title":"Cyber-physical systems security: Limitations, issues and future trends","title-short":"Cyber-physical systems security","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S0141933120303689","volume":"77"},
  {"id":"yangDiffusionModelsComprehensive2022","author":[{"family":"Yang","given":"Ling"},{"family":"Zhang","given":"Zhilong"},{"family":"Song","given":"Yang"},{"family":"Hong","given":"Shenda"},{"family":"Xu","given":"Runsheng"},{"family":"Zhao","given":"Yue"},{"family":"Shao","given":"Yingxia"},{"family":"Zhang","given":"Wentao"},{"family":"Cui","given":"Bin"},{"family":"Yang","given":"Ming-Hsuan"}],"citation-key":"yangDiffusionModelsComprehensive2022","container-title":"arXiv preprint arXiv:2209.00796","issued":{"date-parts":[["2022"]]},"title":"Diffusion models: A comprehensive survey of methods and applications","type":"article-journal"},
+  {"id":"yangDiffusionModelsComprehensive2023","abstract":"Diffusion models have emerged as a powerful new family of deep generative models with record-breaking performance in many applications, including image synthesis, video generation, and molecule design. In this survey, we provide an overview of the rapidly expanding body of work on diffusion models, categorizing the research into three key areas: efficient sampling, improved likelihood estimation, and handling data with special structures. We also discuss the potential for combining diffusion models with other generative models for enhanced results. We further review the wide-ranging applications of diffusion models in fields spanning from computer vision, natural language processing, temporal data modeling, to interdisciplinary applications in other scientific disciplines. This survey aims to provide a contextualized, in-depth look at the state of diffusion models, identifying the key areas of focus and pointing to potential areas for further exploration. Github:","accessed":{"date-parts":[["2024",10,1]]},"author":[{"family":"Yang","given":"Ling"},{"family":"Zhang","given":"Zhilong"},{"family":"Song","given":"Yang"},{"family":"Hong","given":"Shenda"},{"family":"Xu","given":"Runsheng"},{"family":"Zhao","given":"Yue"},{"family":"Zhang","given":"Wentao"},{"family":"Cui","given":"Bin"},{"family":"Yang","given":"Ming-Hsuan"}],"citation-key":"yangDiffusionModelsComprehensive2023","container-title":"ACM Comput. Surv.","DOI":"10.1145/3626235","ISSN":"0360-0300","issue":"4","issued":{"date-parts":[["2023",11,9]]},"page":"105:1–105:39","source":"ACM Digital Library","title":"Diffusion Models: A Comprehensive Survey of Methods and Applications","title-short":"Diffusion Models","type":"article-journal","URL":"https://doi.org/10.1145/3626235","volume":"56"},
  {"id":"yangDiffusionModelsComprehensive2024","abstract":"Diffusion models have emerged as a powerful new family of deep generative models with record-breaking performance in many applications, including image synthesis, video generation, and molecule design. In this survey, we provide an overview of the rapidly expanding body of work on diffusion models, categorizing the research into three key areas: efficient sampling, improved likelihood estimation, and handling data with special structures. We also discuss the potential for combining diffusion models with other generative models for enhanced results. We further review the wide-ranging applications of diffusion models in fields spanning from computer vision, natural language processing, temporal data modeling, to interdisciplinary applications in other scientific disciplines. This survey aims to provide a contextualized, in-depth look at the state of diffusion models, identifying the key areas of focus and pointing to potential areas for further exploration. Github:\n              https://github.com/YangLing0818/Diffusion-Models-Papers-Survey-Taxonomy","accessed":{"date-parts":[["2024",5,20]]},"author":[{"family":"Yang","given":"Ling"},{"family":"Zhang","given":"Zhilong"},{"family":"Song","given":"Yang"},{"family":"Hong","given":"Shenda"},{"family":"Xu","given":"Runsheng"},{"family":"Zhao","given":"Yue"},{"family":"Zhang","given":"Wentao"},{"family":"Cui","given":"Bin"},{"family":"Yang","given":"Ming-Hsuan"}],"citation-key":"yangDiffusionModelsComprehensive2024","container-title":"ACM Computing Surveys","container-title-short":"ACM Comput. Surv.","DOI":"10.1145/3626235","ISSN":"0360-0300, 1557-7341","issue":"4","issued":{"date-parts":[["2024",4,30]]},"language":"en","page":"1-39","source":"DOI.org (Crossref)","title":"Diffusion Models: A Comprehensive Survey of Methods and Applications","title-short":"Diffusion Models","type":"article-journal","URL":"https://dl.acm.org/doi/10.1145/3626235","volume":"56"},
  {"id":"yangMeasureRiskDecisionmaking2005","abstract":"In this paper we extend the classical decision model under risk to a more general case, in which the state of nature corresponding to each risky action may have its own distribution. More speciﬁcally, we propose an expected utilityentropy (EU-E) measure of risk and a decision-making model based on expected utility and entropy. The EU-E measure of risk reﬂects an individual’s intuitive attitude toward risk. The decision model incorporates the expected utility decision criterion as a special case. Using this decision model, a class of decision problems, which cannot be dealt with the expected utility or mean–variance criterion reasonably, can be solved. Besides, some famous decision paradoxes can be interpreted. This decision model can either serve as a descriptive or a normative decision model involving risk.","accessed":{"date-parts":[["2024",1,26]]},"author":[{"family":"Yang","given":"Jiping"},{"family":"Qiu","given":"Wanhua"}],"citation-key":"yangMeasureRiskDecisionmaking2005","container-title":"European Journal of Operational Research","container-title-short":"European Journal of Operational Research","DOI":"10.1016/j.ejor.2004.01.031","ISSN":"03772217","issue":"3","issued":{"date-parts":[["2005",8]]},"language":"en","page":"792-799","source":"DOI.org (Crossref)","title":"A measure of risk and a decision-making model based on expected utility and entropy","type":"article-journal","URL":"https://linkinghub.elsevier.com/retrieve/pii/S0377221704000773","volume":"164"},
  {"id":"yangRuntimeIntegrityVerification2019","abstract":"The world is moving towards a connected ecosystem of cyber-physical components, which are increasingly deployed in diverse fields, from automobiles, to power grids, city infrastructure, manufacturing, and biomedical systems. Majority of these applications call for physical proximity of users to the system due to the nature of the service (e.g., health care). Both remote (through a network) and physical access to these systems have significantly broadened the attack surface of Cyber-Physical Systems (CPS) by providing increased flexibility to observe and alter the system maliciously. Many such systems are deployed in critical applications requiring a high level of operational integrity. Existing solutions for attack detection and prevention are often not adequate, specifically with respect to emerging vulnerabilities. In this paper, we focus on run-time monitoring of CPS with respect to attacks on hardware and software. In particular, we present the motivation for run-time monitoring and then propose methods for detection of physical attacks on hardware and activation of malicious programs in system software, both of which are severe threats to traditional and emerging applications of CPS. We propose a power-up and runtime hardware-software integrity monitoring of sensing and computing equipment in CPS through continuous observation of various side-channel parameters using a plug-and-play hardware module. We present a systematic framework that includes signature generation and comparison technique through device calibration, noise reduction, and workload analysis. Finally, we present a framework for monitoring two side-channel parameters (namely, power and electromagnetic radiation) to detect component replacement and malicious code execution.","accessed":{"date-parts":[["2023",9,27]]},"author":[{"family":"Yang","given":"Shuo"},{"family":"Alaql","given":"Abdulrahman"},{"family":"Hoque","given":"Tamzidul"},{"family":"Bhunia","given":"Swarup"}],"citation-key":"yangRuntimeIntegrityVerification2019","container-title":"2019 IEEE International Conference on Consumer Electronics (ICCE)","DOI":"10.1109/ICCE.2019.8662071","event-title":"2019 IEEE International Conference on Consumer Electronics (ICCE)","ISSN":"2158-4001","issued":{"date-parts":[["2019",1]]},"page":"1-6","source":"IEEE Xplore","title":"Runtime Integrity Verification in Cyber-physical Systems using Side-Channel Fingerprint","type":"paper-conference","URL":"https://ieeexplore.ieee.org/abstract/document/8662071?casa_token=fcNFHkRNawcAAAAA:vcY_JpTHsFPPEVXy60IB0ScqkGXHkAPpk6IAlr1u6MsgPEtBDgrUpuJv3LeLGYdgpw7Nd3qwsw"},
@ -892,6 +913,7 @@
  {"id":"zhongAnalysisEnergyLaboratory2023","abstract":"Laboratory safety in colleges and universities has received wider attention as a critical annual inspection by the Ministry of Education. The laboratory environment is complex and diverse, with many hazard factors. To effectively prevent the occurrence of laboratory emergencies in universities, the STAMP/STPA model is used to analyze the safety of energy laboratory safety management in a resource-based university. Between 2021 and 2022, we carried out laboratory safety inspection and field observation for a mining resource university in China, and identified 16 unsafe control actions in the field of energy laboratory safety management in the university, and identified ten critical causal factors leading to unsafe control actions. Combining the actual situation of the mining resource university, the short-term countermeasures and long-term countermeasures to improve laboratory safety management are proposed to guarantee the university’s laboratory safety management. Moreover, the research results have suggestions for the construction and development of laboratory safety management at similar universities.","accessed":{"date-parts":[["2023",11,3]]},"author":[{"family":"Zhong","given":"Shuheng"},{"family":"Du","given":"Jinping"},{"family":"Jiang","given":"Xidi"}],"citation-key":"zhongAnalysisEnergyLaboratory2023","container-title":"Sustainability","container-title-short":"Sustainability","DOI":"10.3390/su151511505","ISSN":"2071-1050","issue":"15","issued":{"date-parts":[["2023",7,25]]},"language":"en","page":"11505","source":"DOI.org (Crossref)","title":"Analysis of Energy Laboratory Safety Management in China Based on the System-Theoretic Accident Model and Processes/System Theoretic Process Analysis STAMP/STPA Model","type":"article-journal","URL":"https://www.mdpi.com/2071-1050/15/15/11505","volume":"15"},
  {"id":"zhouDigitalTwinFramework2019","abstract":"Digital twin (DT) framework is introduced in the context of application for power grid online analysis. In the development process of a new power grid real-time online analysis system, an online analysis digital twin (OADT) has been implemented to realize the new online analysis architecture. The OADT approach is presented and its prominent features are discussed. The presentation, discussion, and performance testing are based on a large-scale grid network model (40K+ buses), exported directly from the EMS system of an actual power grid. A plan to apply the OADT approach to digitize power grid dispatching rules is also outlined.","accessed":{"date-parts":[["2022",3,8]]},"author":[{"family":"Zhou","given":"Mike"},{"family":"Yan","given":"Jianfeng"},{"family":"Feng","given":"Donghao"}],"citation-key":"zhouDigitalTwinFramework2019","container-title":"Csee Journal of Power and Energy Systems","container-title-short":"CSEE J. Power Energy Syst.","DOI":"10.17775/CSEEJPES.2018.01460","event-place":"Beijing","ISSN":"2096-0042","issue":"3","issued":{"date-parts":[["2019",9]]},"language":"English","note":"WOS:000511344100012","page":"391-398","publisher":"China Electric Power Research Inst","publisher-place":"Beijing","source":"Web of Science Nextgen","title":"Digital Twin Framework and Its Application to Power Grid Online Analysis","type":"article-journal","URL":"http://www.webofscience.com/wos/woscc/summary/marked/relevance/1?markedListId=List%202","volume":"5"},
  {"id":"zhouNeuralLyapunovControl2022","abstract":"Learning for control of dynamical systems with formal guarantees remains a challenging task. This paper proposes a learning framework to simultaneously stabilize an unknown nonlinear system with a neural controller and learn a neural Lyapunov function to certify a region of attraction (ROA) for the closed-loop system with provable guarantees. The algorithmic structure consists of two neural networks and a satisfiability modulo theories (SMT) solver. The first neural network is responsible for learning the unknown dynamics. The second neural network aims to identify a valid Lyapunov function and a provably stabilizing nonlinear controller. The SMT solver verifies the candidate Lyapunov function satisfies the Lyapunov conditions. We further provide theoretical guarantees of the proposed learning framework and show that the obtained Lyapunov function indeed verifies for the unknown nonlinear system under mild assumptions. We illustrate the effectiveness of the results with a few numerical experiments.","accessed":{"date-parts":[["2024",1,17]]},"author":[{"family":"Zhou","given":"Ruikun"},{"family":"Quartz","given":"Thanin"},{"family":"Sterck","given":"Hans De"},{"family":"Liu","given":"Jun"}],"citation-key":"zhouNeuralLyapunovControl2022","event-title":"Advances in Neural Information Processing Systems","issued":{"date-parts":[["2022",5,16]]},"language":"en","source":"openreview.net","title":"Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees","type":"paper-conference","URL":"https://openreview.net/forum?id=QvlcRh8hd8X"},
+  {"id":"zhouSimultaneousIdentificationNominal1994","abstract":"The problem attacked in this paper is to obtain the smallest model set which is described by nominal model, parametric uncertainty bound, unstructured uncertainty bound and consistent with a number of noise-free input-output data, under the condition that the denominator of the nominal model is prescribed. For the compatibility with the available robust control theory, the unstructured uncertainty is measured by H∞-norm, while the parametric uncertainty is by parameter variation interval. It is shown that the unstructured uncertainty bound will generally increase if the nominal model error uncertainty is completely regarded as unstructured. Moreover, the identification problem is reduced to a convex optimization problem which is computationally tractable.","accessed":{"date-parts":[["2024",10,15]]},"author":[{"family":"Zhou","given":"Tong"},{"family":"Kimura","given":"Hidenori"}],"citation-key":"zhouSimultaneousIdentificationNominal1994","container-title":"Automatica","container-title-short":"Automatica","DOI":"10.1016/0005-1098(94)90117-1","ISSN":"0005-1098","issue":"3","issued":{"date-parts":[["1994",3,1]]},"page":"391-402","source":"ScienceDirect","title":"Simultaneous identification of nominal model, parametric uncertainty and unstructured uncertainty for robust control","type":"article-journal","URL":"https://www.sciencedirect.com/science/article/pii/0005109894901171","volume":"30"},
  {"id":"zimmermanMakingFormalMethods2000","abstract":"Despite their potential, formal methods have had difficulty gaining acceptance in the industrial sector. Some complaints are based on supposed impracticality: many consider formal methods to be an approach to system specification and analysis that requires a large learning time. Contributing to this scepticism is the fact that some types of formal methods have not yet been proven to handle systems of realistic complexity. To learn more about how to design formal specification languages that can be used for complex systems and require minimal training, we developed a formal specification of an English language specification of the vertical flight control system similar to that found in the MD-11. This paper describes the lessons learned from this experience.","author":[{"family":"Zimmerman","given":"M."},{"family":"Rodriguez","given":"M."},{"family":"Ingram","given":"B."},{"family":"Katahira","given":"M."},{"family":"Villepin","given":"M.","non-dropping-particle":"de"},{"family":"Leveson","given":"N."}],"citation-key":"zimmermanMakingFormalMethods2000","container-title":"19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126)","DOI":"10.1109/DASC.2000.886879","event-title":"19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126)","issued":{"date-parts":[["2000",10]]},"page":"1B2/1-1B2/8 vol.1","source":"IEEE Xplore","title":"Making formal methods practical","type":"paper-conference","volume":"1"},
  {"id":"zonouzDetectingIndustrialControl2014","accessed":{"date-parts":[["2023",10,10]]},"author":[{"family":"Zonouz","given":"Saman"},{"family":"Rrushi","given":"Julian"},{"family":"McLaughlin","given":"Stephen"}],"citation-key":"zonouzDetectingIndustrialControl2014","container-title":"IEEE Security & Privacy","container-title-short":"IEEE Secur. Privacy","DOI":"10.1109/MSP.2014.113","ISSN":"1540-7993, 1558-4046","issue":"6","issued":{"date-parts":[["2014",11]]},"language":"en","page":"40-47","source":"DOI.org (Crossref)","title":"Detecting Industrial Control Malware Using Automated PLC Code Analytics","type":"article-journal","URL":"https://ieeexplore.ieee.org/document/7006408/","volume":"12"},
  {"id":"ZoteroConnectors","accessed":{"date-parts":[["2024",7,2]]},"citation-key":"ZoteroConnectors","title":"Zotero | Connectors","type":"webpage","URL":"https://www.zotero.org/download/connectors"},
--- a/Stuff/0.
+++ b/Stuff/0.
@ -1,4 +1,4 @@
- [<] Read email from Dr. Cho with shared documents 📅 2024-09-25 ⏳ 2024-09-25 
+- [x] Read email from Dr. Cho with shared documents 📅 2024-09-25 ⏳ 2024-09-25 [completion:: 2024-10-16]
 - [x] Find papers on verifying robustness⏳ 2024-10-15 📅 2024-10-16 [completion:: 2024-10-15]
 - [ ] Start writing about diffusion model📅 2024-10-15 
 - [ ] Write about how to generate unstructured perturbations📅 2024-10-15