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
License
This work is licensed under a Creative Commons Attribution-NonCommercial-Share Alike 4.0 International License.
Recommended Citation
Nguyen, Luan Viet, "CYBER-PHYSICAL SYSTEMS: FROM SPECIFICATION INFERENCE TO DESIGN ANALYSIS" (2018). Computer Science and Engineering Dissertations. 323.
https://mavmatrix.uta.edu/cse_dissertations/323
Comments
Degree granted by The University of Texas at Arlington