Graduation Semester and Year

2018

Language

English

Document Type

Dissertation

Degree Name

Doctor of Philosophy in Computer Engineering

Department

Computer Science and Engineering

First Advisor

Christoph Csallner

Abstract

Due to the high degree of uncertainty and complexity, design and analysis of cyber-physical systems (CPS) are very challenging tasks. The challenge arises immediately in the early CPS development cycle, which is the stage of developing the requirements to capture the desirable behaviors of a system. Missing or incomplete requirements make the CPS design untestable or unverifiable, resulting in CPS failures. Hence, there is an urgent need for the development of specification language as well as specification inference techniques that can efficiently determine formal specifications, well-formulated requirements for CPS. This dissertation presents three different methodologies to determine formal specifications and facilitate the design and analysis of CPS including: 1. the dynamic analysis prototype for automatically identifying cyber-physical specification mismatches of unsafe CPS upgrades, 2. the first study of hyperproperties of real-valued signals, along with a new temporal logic to express them, and 3. the logic-driven classification mechanism to detect abnormal signal behaviors in both time and frequency domains. The above approaches focus on developing formalisms and mining algorithms to formally express and infer many classes of CPS specifications. Based on that, we build a variety of prototypes that can automatically identify specification mismatches arising due to system upgrades, enable simulation-based verification, and detect abnormal model behaviors.

Keywords

Cyber-physical systems, Specification, Design and analysis

Disciplines

Computer Sciences | Physical Sciences and Mathematics

Comments

Degree granted by The University of Texas at Arlington

Download

Share

COinS