Date of Award

Spring 1-1-2016

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Electrical, Computer & Energy Engineering

First Advisor

Sriram Sankaranarayanan

Second Advisor

Fabio Somenzi

Third Advisor

Bor-Yuh Evan Chang

Fourth Advisor

James Kapinski

Fifth Advisor

Jyotirmoy V. Deshmukh

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.

Share

COinS