Graduate Thesis Or Dissertation

 

Reachability Analysis of Cyber-Physical Systems Using Symbolic-Numeric Techniques Public Deposited

Downloadable Content

Download PDF
https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/37720c898
Abstract
  • In this thesis, we address the problem of reachability analysis in cyber-physical systems. These are systems engineered by interfacing computational components with the physical world. They provide partially or fully automated safety-critical services in the form of medical devices, autonomous vehicles, avionics and power systems. We propose techniques to reason about the reachability of such systems, and provide methods for falsifying their safety properties. We model the cyber component as a software program and the physical component as a hybrid dynamical system. Unlike model based analysis, which uses either a purely symbolic or a numerical approach, we argue in favor of using a combination of the two. We justify this by noting that the software program running on a computer is completely specified and has precise semantics. In contrast, the model of the physical system is only an approximation. Hence, we treat the former as a white box, but treat the latter as a black box. Using symbolic methods for the cyber components and numerical methods for hybrid systems, we carefully capture the complex behaviors of software programs and circumvent the difficulty in analyzing complex models developed through first principles. To combine the two techniques, we use a Counterexample Guided Abstraction Refinement (CEGAR) framework. Furthermore, we explore learning techniques like regression and piecewise affine modeling to estimate and represent black box hybrid dynamical systems for the purpose of falsification. We use prototype implementations to demonstrate the effectiveness of presented ideas. Using non-trivial benchmarks, we compare their performance against the state of the art. We also comment on their applicability and discuss ideas for further improvement.
Creator
Date Issued
  • 2016
Academic Affiliation
Advisor
Committee Member
Degree Grantor
Commencement Year
Subject
Last Modified
  • 2019-11-14
Resource Type
Rights Statement
Language

Relationships

Items