BraceAssertion

runtime verification of cyber-physical systems

Xi Zheng, Christine Julien, Rodion Podorozhny, Franck Cassez

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

9 Citations (Scopus)

Abstract

Cyber-Physical Systems (CPS) have gained wide popularity, however, developing and debugging CPS remain significant challenges. Many bugs are detectable only at runtime under deployment conditions that may be unpredictable or at least unexpected at development time. The current state of the practice of debugging CPS is generally ad hoc, involving trial and error in a real deployment. For increased rigor, it is appealing to bring formal methods to CPS verification. However developers often eschew formal approaches due to complexity and lack of efficiency. This paper presents Brace Assertion, a specification framework based on natural language queries that are automatically converted to a determinitic class of timed automata used for runtime monitoring. To reduce runtime overhead and support properties that reference predicate logic, we use a second monitor automaton to create filtered traces on which to run the analysis using the specification monitor. We evaluate the Brace Assertion framework using a real CPS case study and show that the framework is able to minimize runtime overhead with an increasing number of monitors.

Original languageEnglish
Title of host publicationProceedings - 2015 IEEE 12th International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015
Place of PublicationPicataway, NJ
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages298-306
Number of pages9
ISBN (Electronic)9781467391009, 9781467391016
DOIs
Publication statusPublished - 2015
Event12th IEEE International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015 - Dallas, United States
Duration: 19 Oct 201522 Oct 2015

Other

Other12th IEEE International Conference on Mobile Ad Hoc and Sensor Systems, MASS 2015
CountryUnited States
CityDallas
Period19/10/1522/10/15

Fingerprint Dive into the research topics of 'BraceAssertion: runtime verification of cyber-physical systems'. Together they form a unique fingerprint.

Cite this