Physically informed runtime verification for cyber physical systems

dc.contributor.advisorJulien, Christine, D. Sc.en
dc.contributor.committeeMemberPerry, Dewayneen
dc.contributor.committeeMemberKim, Miryungen
dc.contributor.committeeMemberLongoria, Raulen
dc.contributor.committeeMemberKhurshid, Sarfrazen
dc.creatorZheng, Xi, Ph. D.en 2015en
dc.description.abstractCyber-physical systems (CPS) are an integration of computation with physical processes. CPS have gained popularity both in industry and the research community and are represented by many varied mission critical applications. Debugging CPS is important, but the intertwining of the cyber and physical worlds makes it very difficult. Formal methods, simulation, and testing are not sufficient in guarantee required correctness. Runtime Verification (RV) provides a perfect complement. However the state of the art in RV lacks either efficiency or expressiveness, and very few RV technologies are specifically designed for CPS. The CPS community requires an intuitive, expressive, and practical RV middleware toolset to improve the state of the art. In this proposal, I take an incremental and realistic approach to identify and address the research challenges in CPS verification and validation. Firstly, I carry out a systematic analysis of the state of the art and state of the practice in verifying and validating CPS using a structured on-line survey, semi-structured interviews, and an exhaustive literature review. From the findings obtained, I identify the key research gaps and propose research directions to address these research gaps. My second work is to work on the most pertinent research direction proposed, which is to provide a practical and physically informed runtime verification tool-sets specifically designed for CPS as a sound foundation to the trial and error practice identified as the state of the art in verifying and validating CPS. I create an expressive yet intuitive language (BraceAssertion) to specify CPS properties. I develop a framework (BraceBind) to supplement CPS runtime verification with a real time simulation environment which is able to integrate physical models from various simulation platform. Based on BraceAssertion and BraceBind, which collectively captures the combination of logical content and physical environment, I develop a practical runtime verification framework (Brace), which is efficient, effective, expressive in capturing both local and global properties, and guarantee predictable runtime monitors behavior even with unpredictable surge of events. I evaluate the tool-set with increasingly complex real CPS applications of smart agent systems.en
dc.description.departmentElectrical and Computer Engineeringen
dc.subjectCyber physical systemsen
dc.subjectFormal verificationen
dc.subjectRuntime verificationen
dc.subjectSimulation modelsen
dc.subjectTemporal logicen
dc.subjectTimed automataen
dc.subjectBehaviour driven developmenten
dc.subjectAspect oriented programmingen
dc.titlePhysically informed runtime verification for cyber physical systemsen
dc.typeThesisen and Computer Engineeringen and Computer engineeringen University of Texas at Austinen of Philosophyen

Access full-text files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
2.52 MB
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
1.84 KB
Plain Text