Matching Items (16)
Filtering by
- All Subjects: Cyber-Physical Systems
- All Subjects: Guitar music
- Creators: Fainekos, Georgios
- Creators: Hulihan, Charles
Description
The notion of the safety of a system when placed in an environment with humans and other machines has been one of the primary concerns of practitioners while deploying any cyber-physical system (CPS). Such systems, also called safety-critical systems, need to be exhaustively tested for erroneous behavior. This generates the need for coming up with algorithms that can help ascertain the behavior and safety of the system by generating tests for the system where they are likely to falsify. In this work, three algorithms have been presented that aim at finding falsifying behaviors in cyber-physical Systems. PART-X intelligently partitions while sampling the input space to provide probabilistic point and region estimates of falsification. PYSOAR-C and LS-EMIBO aims at finding falsifying behaviors in gray-box systems when some information about the system is available. Specifically, PYSOAR-C aims to find falsification while maximizing coverage using a two-phase optimization process, while LS-EMIBO aims at exploiting the structure of a requirement to find falsifications with lower computational cost compared to the state-of-the-art. This work also shows the efficacy of the algorithms on a wide range of complex cyber-physical systems. The algorithms presented in this thesis are available as python toolboxes.
ContributorsKhandait, Tanmay Bhaskar (Author) / Pedrielli, Giulia (Thesis advisor) / Fainekos, Georgios (Thesis advisor) / Gopalan, Nakul (Committee member) / Arizona State University (Publisher)
Created2022
Description
There has been exciting progress in the area of Unmanned Aerial Vehicles (UAV) in the last decade, especially for quadrotors due to their nature of easy manipulation and simple structure. A lot of research has been done on achieving autonomous and robust control for quadrotors. Recently researchers have been utilizing linear temporal logic as mission specification language for robot motion planning due to its expressiveness and scalability. Several algorithms have been proposed to achieve autonomous temporal logic planning. Also, several frameworks are designed to compose those discrete planners and continuous controllers to make sure the actual trajectory also satisfies the mission specification. However, most of these works use first-order kinematic models which are not accurate when quadrotors fly at high speed and cannot fully utilize the potential of quadrotors.
This thesis work describes a new design for a hierarchical hybrid controller that is based on a dynamic model and seeks to achieve better performance in terms of speed and accuracy compared with some previous works. Furthermore, the proposed hierarchical controller is making progress towards guaranteed satisfaction of mission specification expressed in Linear Temporal Logic for dynamic systems. An event-driven receding horizon planner is also utilized that aims at distributed and decentralized planning for large-scale navigation scenarios. The benefits of this approach will be demonstrated using simulations results.
This thesis work describes a new design for a hierarchical hybrid controller that is based on a dynamic model and seeks to achieve better performance in terms of speed and accuracy compared with some previous works. Furthermore, the proposed hierarchical controller is making progress towards guaranteed satisfaction of mission specification expressed in Linear Temporal Logic for dynamic systems. An event-driven receding horizon planner is also utilized that aims at distributed and decentralized planning for large-scale navigation scenarios. The benefits of this approach will be demonstrated using simulations results.
ContributorsZhang, Xiaotong (Author) / Fainekos, Georgios (Thesis advisor) / Ben Amor, Heni (Committee member) / Shrivastava, Aviral (Committee member) / Arizona State University (Publisher)
Created2016
Description
Critical infrastructures in healthcare, power systems, and web services, incorporate cyber-physical systems (CPSes), where the software controlled computing systems interact with the physical environment through actuation and monitoring. Ensuring software safety in CPSes, to avoid hazards to property and human life as a result of un-controlled interactions, is essential and challenging. The principal hurdle in this regard is the characterization of the context driven interactions between software and the physical environment (cyber-physical interactions), which introduce multi-dimensional dynamics in space and time, complex non-linearities, and non-trivial aggregation of interaction in case of networked operations. Traditionally, CPS software is tested for safety either through experimental trials, which can be expensive, incomprehensive, and hazardous, or through static analysis of code, which ignore the cyber-physical interactions. This thesis considers model based engineering, a paradigm widely used in different disciplines of engineering, for safety verification of CPS software and contributes to three fundamental phases: a) modeling, building abstractions or models that characterize cyberphysical interactions in a mathematical framework, b) analysis, reasoning about safety based on properties of the model, and c) synthesis, implementing models on standard testbeds for performing preliminary experimental trials. In this regard, CPS modeling techniques are proposed that can accurately capture the context driven spatio-temporal aggregate cyber-physical interactions. Different levels of abstractions are considered, which result in high level architectural models, or more detailed formal behavioral models of CPSes. The outcomes include, a well defined architectural specification framework called CPS-DAS and a novel spatio-temporal formal model called Spatio-Temporal Hybrid Automata (STHA) for CPSes. Model analysis techniques are proposed for the CPS models, which can simulate the effects of dynamic context changes on non-linear spatio-temporal cyberphysical interactions, and characterize aggregate effects. The outcomes include tractable algorithms for simulation analysis and for theoretically proving safety properties of CPS software. Lastly a software synthesis technique is proposed that can automatically convert high level architectural models of CPSes in the healthcare domain into implementations in high level programming languages. The outcome is a tool called Health-Dev that can synthesize software implementations of CPS models in healthcare for experimental verification of safety properties.
ContributorsBanerjee, Ayan (Author) / Gupta, Sandeep K.S. (Thesis advisor) / Poovendran, Radha (Committee member) / Fainekos, Georgios (Committee member) / Maciejewski, Ross (Committee member) / Arizona State University (Publisher)
Created2012
ContributorsCostello, Joseph R. (Performer) / Johnson, Carol (Performer) / Hulihan, Charles (Performer) / ASU Library. Music Library (Publisher)
Created1998-04-05
ContributorsFrancis, Patrick (Performer) / Hulihan, Charles (Performer) / ASU Library. Music Library (Publisher)
Created1996-04-26
ContributorsFrancis, Patrick (Performer) / Hulihan, Charles (Performer) / Clark, Mai (Performer) / King, Spenser (Performer) / ASU Library. Music Library (Publisher)
Created1995-04-22