Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems

Houssam Abbas, Bardh Hoxha, Georgios Fainekos, Koichi Ueda

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

20 Scopus citations

Abstract

We present a framework for automatic specification-guided testing for Stochastic Cyber-Physical Systems (SCPS). The framework utilizes the theory of robustness of Metric Temporal Logic (MTL) specifications to quantify how robustly an SCPS satisfies a specification in MTL. The goal of the testing framework is to detect system operating conditions that cause the system to exhibit the worst expected specification robustness. The resulting expected robustness minimization problem is solved using Markov chain Monte Carlo algorithms. This also allows us to use finite-time guarantees, which quantify the quality of the solution after a finite number of simulations. In a Model-Based Design (MBD) process, our framework can be combined with Statistical Model Checking (SMC). Finally, we present a case study on a high fidelity engine model where the goal is to verify the air-to-fuel ratio problem.

Original languageEnglish (US)
Title of host publication4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1-6
Number of pages6
ISBN (Electronic)9781479936687
DOIs
StatePublished - Oct 7 2014
Event4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014 - Hong Kong, China
Duration: Jun 4 2014Jun 7 2014

Publication series

Name4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014

Other

Other4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014
CountryChina
CityHong Kong
Period6/4/146/7/14

ASJC Scopus subject areas

  • Artificial Intelligence
  • Information Systems
  • Control and Systems Engineering
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems'. Together they form a unique fingerprint.

Cite this