Showing 1–22 of 22 results for author: Bakirtzis, G

Navigating the sociotechnical labyrinth: Dynamic certification for responsible embodied AI

Authors: Georgios Bakirtzis, Andrea Aler Tubella, Andreas Theodorou, David Danks, Ufuk Topcu

Abstract: Sociotechnical requirements shape the governance of artificially intelligent (AI) systems. In an era where embodied AI technologies are rapidly reshaping various facets of contemporary society, their inherent dynamic adaptability presents a unique blend of opportunities and challenges. Traditional regulatory mechanisms, often designed for static -- or slower-paced -- technologies, find themselves… ▽ More Sociotechnical requirements shape the governance of artificially intelligent (AI) systems. In an era where embodied AI technologies are rapidly reshaping various facets of contemporary society, their inherent dynamic adaptability presents a unique blend of opportunities and challenges. Traditional regulatory mechanisms, often designed for static -- or slower-paced -- technologies, find themselves at a crossroads when faced with the fluid and evolving nature of AI systems. Moreover, typical problems in AI, for example, the frequent opacity and unpredictability of the behaviour of the systems, add additional sociotechnical challenges. To address these interconnected issues, we introduce the concept of dynamic certification, an adaptive regulatory framework specifically crafted to keep pace with the continuous evolution of AI systems. The complexity of these challenges requires common progress in multiple domains: technical, socio-governmental, and regulatory. Our proposed transdisciplinary approach is designed to ensure the safe, ethical, and practical deployment of AI systems, aligning them bidirectionally with the real-world contexts in which they operate. By doing so, we aim to bridge the gap between rapid technological advancement and effective regulatory oversight, ensuring that AI systems not only achieve their intended goals but also adhere to ethical standards and societal values. △ Less

Submitted 16 August, 2024; originally announced September 2024.

Reduce, Reuse, Recycle: Categories for Compositional Reinforcement Learning

Authors: Georgios Bakirtzis, Michail Savvas, Ruihan Zhao, Sandeep Chinchali, Ufuk Topcu

Abstract: In reinforcement learning, conducting task composition by forming cohesive, executable sequences from multiple tasks remains challenging. However, the ability to (de)compose tasks is a linchpin in developing robotic systems capable of learning complex behaviors. Yet, compositional reinforcement learning is beset with difficulties, including the high dimensionality of the problem space, scarcity of… ▽ More In reinforcement learning, conducting task composition by forming cohesive, executable sequences from multiple tasks remains challenging. However, the ability to (de)compose tasks is a linchpin in developing robotic systems capable of learning complex behaviors. Yet, compositional reinforcement learning is beset with difficulties, including the high dimensionality of the problem space, scarcity of rewards, and absence of system robustness after task composition. To surmount these challenges, we view task composition through the prism of category theory -- a mathematical discipline exploring structures and their compositional relationships. The categorical properties of Markov decision processes untangle complex tasks into manageable sub-tasks, allowing for strategical reduction of dimensionality, facilitating more tractable reward structures, and bolstering system robustness. Experimental results support the categorical theory of reinforcement learning by enabling skill reduction, reuse, and recycling when learning complex robotic arm tasks. △ Less

Submitted 11 March, 2025; v1 submitted 23 August, 2024; originally announced August 2024.

Comments: ECAI 2024

Negotiating Control: Neurosymbolic Variable Autonomy

Authors: Georgios Bakirtzis, Manolis Chiou, Andreas Theodorou

Abstract: Variable autonomy equips a system, such as a robot, with mixed initiatives such that it can adjust its independence level based on the task's complexity and the surrounding environment. Variable autonomy solves two main problems in robotic planning: the first is the problem of humans being unable to keep focus in monitoring and intervening during robotic tasks without appropriate human factor indi… ▽ More Variable autonomy equips a system, such as a robot, with mixed initiatives such that it can adjust its independence level based on the task's complexity and the surrounding environment. Variable autonomy solves two main problems in robotic planning: the first is the problem of humans being unable to keep focus in monitoring and intervening during robotic tasks without appropriate human factor indicators, and the second is achieving mission success in unforeseen and uncertain environments in the face of static reward structures. An open problem in variable autonomy is developing robust methods to dynamically balance autonomy and human intervention in real-time, ensuring optimal performance and safety in unpredictable and evolving environments. We posit that addressing unpredictable and evolving environments through an addition of rule-based symbolic logic has the potential to make autonomy adjustments more contextually reliable and adding feedback to reinforcement learning through data from mixed-initiative control further increases efficacy and safety of autonomous behaviour. △ Less

Submitted 23 July, 2024; originally announced July 2024.

Formal Methods for Autonomous Systems

Authors: Tichakorn Wongpiromsarn, Mahsa Ghasemi, Murat Cubuktepe, Georgios Bakirtzis, Steven Carr, Mustafa O. Karabag, Cyrus Neary, Parham Gohari, Ufuk Topcu

Abstract: Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. Th… ▽ More Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification. △ Less

Submitted 2 November, 2023; originally announced November 2023.

Sensor Placement for Online Fault Diagnosis

Authors: Dhananjay Raju, Georgios Bakirtzis, Ufuk Topcu

Abstract: Fault diagnosis is the problem of determining a set of faulty system components that explain discrepancies between observed and expected behavior. Due to the intrinsic relation between observations and sensors placed on a system, sensors' fault diagnosis and placement are mutually dependent. Consequently, it is imperative to solve the fault diagnosis and sensor placement problems jointly. One appr… ▽ More Fault diagnosis is the problem of determining a set of faulty system components that explain discrepancies between observed and expected behavior. Due to the intrinsic relation between observations and sensors placed on a system, sensors' fault diagnosis and placement are mutually dependent. Consequently, it is imperative to solve the fault diagnosis and sensor placement problems jointly. One approach to modeling systems for fault diagnosis uses answer set programming (ASP). We present a model-based approach to sensor placement for active diagnosis using ASP, where the secondary objective is to reduce the number of sensors used. The proposed method finds locations for system sensors with around 500 components in a few minutes. To address larger systems, we propose a notion of modularity such that it is possible to treat each module as a separate system and solve the sensor placement problem for each module independently. Additionally, we provide a fixpoint algorithm for determining the modules of a system. △ Less

Submitted 21 November, 2022; originally announced November 2022.

A formal process of hierarchical functional requirements development for Set-Based Design

Authors: Minghui Sun, Zhaoyang Chen, Georgios Bakirtzis, Hassan Jafarzadeh, Cody Fleming

Abstract: The design of complex systems is typically uncertain and ambiguous at early stages. Set-Based Design is a promising approach to complex systems design as it supports alternative exploration and gradual uncertainty reduction. When designing a complex system, functional requirements decomposition is a common and effective approach to progress the design incrementally. However, the current literature… ▽ More The design of complex systems is typically uncertain and ambiguous at early stages. Set-Based Design is a promising approach to complex systems design as it supports alternative exploration and gradual uncertainty reduction. When designing a complex system, functional requirements decomposition is a common and effective approach to progress the design incrementally. However, the current literature on Set-Based Design lacks formal guidance in functional requirements decomposition. To bridge the gap, we propose a formal process to hierarchically decompose the functional requirements for Set-Based Design. A four-step formal process is proposed to systematically define, reason, and narrow the sets, and eventually decompose the functional requirement into the sub-requirements. Such a process can be used by the individual suppliers working in parallel at multiple levels of abstraction and guarantee that the resulting system will eventually satisfy the top-level functional requirements. An example of designing a cruise control system is applied to demonstrate the feasibility of the proposed process. △ Less

Submitted 25 October, 2022; originally announced October 2022.

Categorical semantics of compositional reinforcement learning

Authors: Georgios Bakirtzis, Michail Savvas, Ufuk Topcu

Abstract: Compositional knowledge representations in reinforcement learning (RL) facilitate modular, interpretable, and safe task specifications. However, generating compositional models requires the characterization of minimal assumptions for the robustness of the compositionality feature, especially in the case of functional decompositions. Using a categorical point of view, we develop a knowledge represe… ▽ More Compositional knowledge representations in reinforcement learning (RL) facilitate modular, interpretable, and safe task specifications. However, generating compositional models requires the characterization of minimal assumptions for the robustness of the compositionality feature, especially in the case of functional decompositions. Using a categorical point of view, we develop a knowledge representation framework for a compositional theory of RL. Our approach relies on the theoretical study of the category $\mathsf{MDP}$, whose objects are Markov decision processes (MDPs) acting as models of tasks. The categorical semantics models the compositionality of tasks through the application of pushout operations akin to combining puzzle pieces. As a practical application of these pushout operations, we introduce zig-zag diagrams that rely on the compositional guarantees engendered by the category $\mathsf{MDP}$. We further prove that properties of the category $\mathsf{MDP}$ unify concepts, such as enforcing safety requirements and exploiting symmetries, generalizing previous abstraction theories for RL. △ Less

Submitted 10 March, 2025; v1 submitted 29 August, 2022; originally announced August 2022.

AC-feasible Local Flexibility Market with Continuous Trading

Authors: Aikaterini A. Forouli, Georgios K. Papazoglou, Emmanouil A. Bakirtzis, Pandelis N. Biskas, Anastasios G. Bakirtzis

Abstract: This paper proposes a novel continuous Local Flexibility Market where active power flexibility located in the distribution system can be traded. The market design engages the Market Operator, the Distribution System Operator and Market Participants with dispatchable assets. The proposed market operates in a single distribution system and considers network constraints via AC network sensitivities,… ▽ More This paper proposes a novel continuous Local Flexibility Market where active power flexibility located in the distribution system can be traded. The market design engages the Market Operator, the Distribution System Operator and Market Participants with dispatchable assets. The proposed market operates in a single distribution system and considers network constraints via AC network sensitivities, calculated at an initial network operating point. Trading is possible when AC network constraints are respected and when anticipated network violations are alleviated or resolved. The implementation allows for partial bid matching and is computationally light, therefore, suitable for continuous trading applications. The proposed design is thoroughly described and is demonstrated in a test distribution system. It is shown that active power trading in the proposed market design can lead to resolution of line overloads. △ Less

Submitted 12 July, 2022; originally announced July 2022.

Comments: In proceedings of the 11th Bulk Power Systems Dynamics and Control Symposium (IREP 2022), July 25-30, 2022, Banff, Canada

Report number: IREP2022-24

STPA-driven Multilevel Runtime Monitoring for In-time Hazard Detection

Authors: Smitha Gautham, Georgios Bakirtzis, Alexander Will, Athira V. Jayakumar, Carl R. Elks

Abstract: Runtime verification or runtime monitoring equips safety-critical cyber-physical systems to augment design assurance measures and ensure operational safety and security. Cyber-physical systems have interaction failures, attack surfaces, and attack vectors resulting in unanticipated hazards and loss scenarios. These interaction failures pose challenges to runtime verification regarding monitoring s… ▽ More Runtime verification or runtime monitoring equips safety-critical cyber-physical systems to augment design assurance measures and ensure operational safety and security. Cyber-physical systems have interaction failures, attack surfaces, and attack vectors resulting in unanticipated hazards and loss scenarios. These interaction failures pose challenges to runtime verification regarding monitoring specifications and monitoring placements for in-time detection of hazards. We develop a well-formed workflow model that connects system theoretic process analysis, commonly referred to as STPA, hazard causation information to lower-level runtime monitoring to detect hazards at the operational phase. Specifically, our model follows the DepDevOps paradigm to provide evidence and insights to runtime monitoring on what to monitor, where to monitor, and the monitoring context. We demonstrate and evaluate the value of multilevel monitors by injecting hazards on an autonomous emergency braking system model. △ Less

Submitted 22 June, 2022; v1 submitted 19 April, 2022; originally announced April 2022.

AlgebraicSystems: Compositional Verification for Autonomous System Design

Authors: Georgios Bakirtzis, Ufuk Topcu

Abstract: Autonomous systems require the management of several model views to assure properties such as safety and security among others. A crucial issue in autonomous systems design assurance is the notion of emergent behavior; we cannot use their parts in isolation to examine their overall behavior or performance. Compositional verification attempts to combat emergence by implementing model transformation… ▽ More Autonomous systems require the management of several model views to assure properties such as safety and security among others. A crucial issue in autonomous systems design assurance is the notion of emergent behavior; we cannot use their parts in isolation to examine their overall behavior or performance. Compositional verification attempts to combat emergence by implementing model transformation as structure-preserving maps between model views. AlgebraicDynamics relies on categorical semantics to draw relationships between algebras and model views. We propose AlgebraicSystems, a conglomeration of algebraic methods to assign semantics and categorical primitives to give computational meaning to relationships between models so that the formalisms and resulting tools are interoperable through vertical and horizontal composition. △ Less

Submitted 3 March, 2022; originally announced March 2022.

Dynamic Certification for Autonomous Systems

Authors: Georgios Bakirtzis, Steven Carr, David Danks, Ufuk Topcu

Abstract: Autonomous systems are often deployed in complex sociotechnical environments, such as public roads, where they must behave safely and securely. Unlike many traditionally engineered systems, autonomous systems are expected to behave predictably in varying "open world" environmental contexts that cannot be fully specified formally. As a result, assurance about autonomous systems requires us to devel… ▽ More Autonomous systems are often deployed in complex sociotechnical environments, such as public roads, where they must behave safely and securely. Unlike many traditionally engineered systems, autonomous systems are expected to behave predictably in varying "open world" environmental contexts that cannot be fully specified formally. As a result, assurance about autonomous systems requires us to develop new certification methods and mathematical tools that can bound the uncertainty engendered by these diverse deployment scenarios, rather than relying on static tools. △ Less

Submitted 25 April, 2023; v1 submitted 21 March, 2022; originally announced March 2022.

Compositional Cyber-Physical Systems Theory

Authors: Georgios Bakirtzis

Abstract: This dissertation builds a compositional cyber-physical systems theory to develop concrete semantics relating the above diverse views necessary for safety and security assurance. In this sense, composition can take two forms. The first is composing larger models from smaller ones within each individual formalism of requirements, behaviors, and architectures which can be thought of as horizontal co… ▽ More This dissertation builds a compositional cyber-physical systems theory to develop concrete semantics relating the above diverse views necessary for safety and security assurance. In this sense, composition can take two forms. The first is composing larger models from smaller ones within each individual formalism of requirements, behaviors, and architectures which can be thought of as horizontal composition -- a problem which is largely solved. The second and main contribution of this theory is vertical composition, meaning relating or otherwise providing verified composition across requirement, behavioral, and architecture models and their associated algebras. In this dissertation, we show that one possible solution to vertical composition is to use tools from category theory. Category theory is a natural candidate for making both horizontal and vertical composition formally explicit because it can relate, compare, and/or unify different algebras. △ Less

Submitted 10 September, 2021; originally announced September 2021.

Comments: PhD thesis

Compositional Thinking in Cyberphysical Systems Theory

Authors: Georgios Bakirtzis, Eswaran Subrahmanian, Cody H. Fleming

Abstract: Engineering safe and secure cyber-physical systems requires system engineers to develop and maintain a number of model views, both dynamic and static, which can be seen as algebras. We posit that verifying the composition of requirement, behavioral, and architectural models using category theory gives rise to a strictly compositional interpretation of cyber-physical systems theory, which can assis… ▽ More Engineering safe and secure cyber-physical systems requires system engineers to develop and maintain a number of model views, both dynamic and static, which can be seen as algebras. We posit that verifying the composition of requirement, behavioral, and architectural models using category theory gives rise to a strictly compositional interpretation of cyber-physical systems theory, which can assist in the modeling and analysis of safety-critical cyber-physical systems. △ Less

Submitted 9 October, 2021; v1 submitted 26 May, 2021; originally announced May 2021.

Yoneda Hacking: The Algebra of Attacker Actions

Authors: Georgios Bakirtzis, Fabrizio Genovese, Cody H. Fleming

Abstract: Our work focuses on modeling the security of systems from their component-level designs. Towards this goal, we develop a categorical formalism to model attacker actions. Equipping the categorical formalism with algebras produces two interesting results for security modeling. First, using the Yoneda lemma, we can model attacker reconnaissance missions. In this context, the Yoneda lemma shows us tha… ▽ More Our work focuses on modeling the security of systems from their component-level designs. Towards this goal, we develop a categorical formalism to model attacker actions. Equipping the categorical formalism with algebras produces two interesting results for security modeling. First, using the Yoneda lemma, we can model attacker reconnaissance missions. In this context, the Yoneda lemma shows us that if two system representations, one being complete and the other being the attacker's incomplete view, agree at every possible test, they behave the same. The implication is that attackers can still successfully exploit the system even with incomplete information. Second, we model the potential changes to the system via an exploit. An exploit either manipulates the interactions between system components, such as providing the wrong values to a sensor, or changes the components themselves, such as controlling a global positioning system (GPS). One additional benefit of using category theory is that mathematical operations can be represented as formal diagrams, helpful in applying this analysis in a model-based design setting. We illustrate this modeling framework using an unmanned aerial vehicle (UAV) cyber-physical system model. We demonstrate and model two types of attacks (1) a rewiring attack, which violates data integrity, and (2) a rewriting attack, which violates availability. △ Less

Submitted 13 April, 2022; v1 submitted 26 February, 2021; originally announced March 2021.

Compositional Cyber-Physical Systems Modeling

Authors: Georgios Bakirtzis, Christina Vasilakopoulou, Cody H. Fleming

Abstract: Assuring the correct behavior of cyber-physical systems requires significant modeling effort, particularly during early stages of the engineering and design process when a system is not yet available for testing or verification of proper behavior. A primary motivation for `getting things right' in these early design stages is that altering the design is significantly less costly and more effective… ▽ More Assuring the correct behavior of cyber-physical systems requires significant modeling effort, particularly during early stages of the engineering and design process when a system is not yet available for testing or verification of proper behavior. A primary motivation for `getting things right' in these early design stages is that altering the design is significantly less costly and more effective than when hardware and software have already been developed. Engineering cyber-physical systems requires the construction of several different types of models, each representing a different view, which include stakeholder requirements, system behavior, and the system architecture. Furthermore, each of these models can be represented at different levels of abstraction. Formal reasoning has improved the precision and expanded the available types of analysis in assuring correctness of requirements, behaviors, and architectures. However, each is usually modeled in distinct formalisms and corresponding tools. Currently, this disparity means that a system designer must manually check that the different models are in agreement. Manually editing and checking models is error prone, time consuming, and sensitive to any changes in the design of the models themselves. Wiring diagrams and related theory provide a means for formally organizing these different but related modeling views, resulting in a compositional modeling language for cyber-physical systems. Such a categorical language can make concrete the relationship between different model views, thereby managing complexity, allowing hierarchical decomposition of system models, and formally proving consistency between models. △ Less

Submitted 25 January, 2021; originally announced January 2021.

Comments: In Proceedings ACT 2020, arXiv:2101.07888

Journal ref: EPTCS 333, 2021, pp. 125-138

Cyberphysical Security Through Resiliency: A Systems-centric Approach

Authors: Cody Fleming, Carl Elks, Georgios Bakirtzis, Stephen C. Adams, Bryan Carter, Peter A. Beling, Barry Horowitz

Abstract: Cyber-physical systems (CPS) are often defended in the same manner as information technology (IT) systems -- by using perimeter security. Multiple factors make such defenses insufficient for CPS. Resiliency shows potential in overcoming these shortfalls. Techniques for achieving resilience exist; however, methods and theory for evaluating resilience in CPS are lacking. We argue that such methods a… ▽ More Cyber-physical systems (CPS) are often defended in the same manner as information technology (IT) systems -- by using perimeter security. Multiple factors make such defenses insufficient for CPS. Resiliency shows potential in overcoming these shortfalls. Techniques for achieving resilience exist; however, methods and theory for evaluating resilience in CPS are lacking. We argue that such methods and theory should assist stakeholders in deciding where and how to apply design patterns for resilience. Such a problem potentially involves tradeoffs between different objectives and criteria, and such decisions need to be driven by traceable, defensible, repeatable engineering evidence. Multi-criteria resiliency problems require a system-oriented approach that evaluates systems in the presence of threats as well as potential design solutions once vulnerabilities have been identified. We present a systems-oriented view of cyber-physical security, termed Mission Aware, that is based on a holistic understanding of mission goals, system dynamics, and risk. △ Less

Submitted 9 October, 2021; v1 submitted 29 November, 2020; originally announced November 2020.

Categorical Semantics of Cyber-Physical Systems Theory

Authors: Georgios Bakirtzis, Cody H. Fleming, Christina Vasilakopoulou

Abstract: Cyber-physical systems require the construction and management of various models to assure their correct, safe, and secure operation. These various models are necessary because of the coupled physical and computational dynamics present in cyber-physical systems. However, to date the different model views of cyber-physical systems are largely related informally, which raises issues with the degree… ▽ More Cyber-physical systems require the construction and management of various models to assure their correct, safe, and secure operation. These various models are necessary because of the coupled physical and computational dynamics present in cyber-physical systems. However, to date the different model views of cyber-physical systems are largely related informally, which raises issues with the degree of formal consistency between those various models of requirements, system behavior, and system architecture. We present a category-theoretic framework to make different types of composition explicit in the modeling and analysis of cyber-physical systems, which could assist in verifying the system as a whole. This compositional framework for cyber-physical systems gives rise to unified system models, where system behavior is hierarchically decomposed and related to a system architecture using the systems-as-algebras paradigm. As part of this paradigm, we show that an algebra of (safety) contracts generalizes over the state of the art, providing more uniform mathematical tools for constraining the behavior over a richer set of composite cyber-physical system models, which has the potential of minimizing or eliminating hazardous behavior. △ Less

Submitted 26 April, 2021; v1 submitted 15 October, 2020; originally announced October 2020.

An Ontological Metamodel for Cyber-Physical System Safety, Security, and Resilience Coengineering

Authors: Georgios Bakirtzis, Tim Sherburne, Stephen Adams, Barry M. Horowitz, Peter A. Beling, Cody H. Fleming

Abstract: System complexity has become ubiquitous in the design, assessment, and implementation of practical and useful cyber-physical systems. This increased complexity is impacting the management of models necessary for designing cyber-physical systems that are able to take into account a number of ``-ilities'', such that they are safe and secure and ultimately resilient to disruption of service. We propo… ▽ More System complexity has become ubiquitous in the design, assessment, and implementation of practical and useful cyber-physical systems. This increased complexity is impacting the management of models necessary for designing cyber-physical systems that are able to take into account a number of ``-ilities'', such that they are safe and secure and ultimately resilient to disruption of service. We propose an ontological metamodel for system design that augments an already existing industry metamodel to capture the relationships between various model elements and safety, security, and resilient considerations. Employing this metamodel leads to more cohesive and structured modeling efforts with an overall increase in scalability, usability, and unification of already existing models. In turn, this leads to a mission-oriented perspective in designing security defenses and resilience mechanisms to combat undesirable behaviors. We illustrate this metamodel in an open-source GraphQL implementation, which can interface with a number of modeling languages. We support our proposed metamodel with a detailed demonstration using an oil and gas pipeline model. △ Less

Submitted 9 June, 2020; originally announced June 2020.

Fundamental Challenges of Cyber-Physical Systems Security Modeling

Authors: Georgios Bakirtzis, Garrett L. Ward, Christopher J. Deloglos, Carl R. Elks, Barry M. Horowitz, Cody H. Fleming

Abstract: Systems modeling practice lacks security analysis tools that can interface with modeling languages to facilitate security by design. Security by design is a necessity in the age of safety critical cyber-physical systems, where security violations can cause hazards. Currently, the overlap between security and safety is narrow. But deploying cyber-physical systems means that today's adversaries can… ▽ More Systems modeling practice lacks security analysis tools that can interface with modeling languages to facilitate security by design. Security by design is a necessity in the age of safety critical cyber-physical systems, where security violations can cause hazards. Currently, the overlap between security and safety is narrow. But deploying cyber-physical systems means that today's adversaries can intentionally trigger accidents. By implementing security assessment tools for modeling languages we are better able to address threats earlier in the system's lifecycle and, therefore, assure their safe and secure behavior in their eventual deployment. We posit that cyber-physical systems security modeling is practiced insufficiently because it is still addressed similarly to information technology systems. △ Less

Submitted 30 April, 2020; originally announced May 2020.

Data Driven Vulnerability Exploration for Design Phase System Analysis

Authors: Georgios Bakirtzis, Brandon J. Simon, Aidan G. Collins, Cody H. Fleming, Carl R. Elks

Abstract: Applying security as a lifecycle practice is becoming increasingly important to combat targeted attacks in safety-critical systems. Among others there are two significant challenges in this area: (1) the need for models that can characterize a realistic system in the absence of an implementation and (2) an automated way to associate attack vector information; that is, historical data, to such syst… ▽ More Applying security as a lifecycle practice is becoming increasingly important to combat targeted attacks in safety-critical systems. Among others there are two significant challenges in this area: (1) the need for models that can characterize a realistic system in the absence of an implementation and (2) an automated way to associate attack vector information; that is, historical data, to such system models. We propose the cybersecurity body of knowledge (CYBOK), which takes in sufficiently characteristic models of systems and acts as a search engine for potential attack vectors. CYBOK is fundamentally an algorithmic approach to vulnerability exploration, which is a significant extension to the body of knowledge it builds upon. By using CYBOK, security analysts and system designers can work together to assess the overall security posture of systems early in their lifecycle, during major design decisions and before final product designs. Consequently, assisting in applying security earlier and throughout the systems lifecycle. △ Less

Submitted 6 September, 2019; originally announced September 2019.

Correct-by-construction requirement decomposition

Authors: Minghui Sun, Georgios Bakirtzis, Hassan Jafarzadeh, Cody Fleming

Abstract: In systems engineering, accurately decomposing requirements is crucial for creating well-defined and manageable system components, particularly in safety-critical domains. Despite the critical need, rigorous, top-down methodologies for effectively breaking down complex requirements into precise, actionable sub-requirements are scarce, especially compared to the wealth of bottom-up verification tec… ▽ More In systems engineering, accurately decomposing requirements is crucial for creating well-defined and manageable system components, particularly in safety-critical domains. Despite the critical need, rigorous, top-down methodologies for effectively breaking down complex requirements into precise, actionable sub-requirements are scarce, especially compared to the wealth of bottom-up verification techniques. Addressing this gap, we introduce a formal decomposition for contract-based design that guarantees the correctness of decomposed requirements if specific conditions are met. Our (semi-)automated methodology augments contract-based design with reachability analysis and constraint programming to systematically identify, verify, and validate sub-requirements representable by continuous bounded sets -- continuous relations between real-valued inputs and outputs. We demonstrate the efficacy and practicality of a correct-by-construction approach through a comprehensive case study on a cruise control system, highlighting how our methodology improves the interpretability, tractability, and verifiability of system requirements. △ Less

Submitted 14 May, 2025; v1 submitted 4 September, 2019; originally announced September 2019.

A Model-Based Approach to Security Analysis for Cyber-Physical Systems

Authors: Georgios Bakirtzis, Bryan T. Carter, Carl R. Elks, Cody H. Fleming

Abstract: Evaluating the security of cyber-physical systems throughout their life cycle is necessary to assure that they can be deployed and operated in safety-critical applications, such as infrastructure, military, and transportation. Most safety and security decisions that can have major effects on mitigation strategy options after deployment are made early in the system's life cycle. To allow for a vuln… ▽ More Evaluating the security of cyber-physical systems throughout their life cycle is necessary to assure that they can be deployed and operated in safety-critical applications, such as infrastructure, military, and transportation. Most safety and security decisions that can have major effects on mitigation strategy options after deployment are made early in the system's life cycle. To allow for a vulnerability analysis before deployment, a sufficient well-formed model has to be constructed. To construct such a model we produce a taxonomy of attributes; that is, a generalized schema for system attributes. This schema captures the necessary specificity that characterizes a possible real system and can also map to the attack vector space associated with the model's attributes. In this way, we can match possible attack vectors and provide architectural mitigation at the design phase. We present a model of a flight control system encoded in the Systems Modeling Language, commonly known as SysML, but also show agnosticism with respect to the modeling language or tool used. △ Less

Submitted 10 June, 2018; v1 submitted 31 October, 2017; originally announced October 2017.

Comments: 8 pages, 5 figures, conference