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

14 Citations (Scopus)

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 (Print)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

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

Fingerprint

Temporal logic
Specifications
Testing
Model checking
Markov processes
Engines
Cyber Physical System
Air

ASJC Scopus subject areas

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

Cite this

Abbas, H., Hoxha, B., Fainekos, G., & Ueda, K. (2014). Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems. In 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014 (pp. 1-6). [6917426] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CYBER.2014.6917426

Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems. / Abbas, Houssam; Hoxha, Bardh; Fainekos, Georgios; Ueda, Koichi.

4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014. Institute of Electrical and Electronics Engineers Inc., 2014. p. 1-6 6917426.

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

Abbas, H, Hoxha, B, Fainekos, G & Ueda, K 2014, Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems. in 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014., 6917426, Institute of Electrical and Electronics Engineers Inc., pp. 1-6, 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014, Hong Kong, China, 6/4/14. https://doi.org/10.1109/CYBER.2014.6917426
Abbas H, Hoxha B, Fainekos G, Ueda K. Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems. In 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 1-6. 6917426 https://doi.org/10.1109/CYBER.2014.6917426
Abbas, Houssam ; Hoxha, Bardh ; Fainekos, Georgios ; Ueda, Koichi. / Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems. 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 1-6
@inproceedings{1539803509e1421c8347a53cc0d6d6fd,
title = "Robustness-guided temporal logic testing and verification for Stochastic Cyber-Physical Systems",
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.",
author = "Houssam Abbas and Bardh Hoxha and Georgios Fainekos and Koichi Ueda",
year = "2014",
month = "10",
day = "7",
doi = "10.1109/CYBER.2014.6917426",
language = "English (US)",
isbn = "9781479936687",
pages = "1--6",
booktitle = "4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

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

AU - Abbas, Houssam

AU - Hoxha, Bardh

AU - Fainekos, Georgios

AU - Ueda, Koichi

PY - 2014/10/7

Y1 - 2014/10/7

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84910602225&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84910602225&partnerID=8YFLogxK

U2 - 10.1109/CYBER.2014.6917426

DO - 10.1109/CYBER.2014.6917426

M3 - Conference contribution

SN - 9781479936687

SP - 1

EP - 6

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

PB - Institute of Electrical and Electronics Engineers Inc.

ER -