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
N1 - Publisher Copyright:
© 2014 IEEE.
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
AN - SCOPUS:84910602225
T3 - 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014
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.
T2 - 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent Systems, IEEE-CYBER 2014
Y2 - 4 June 2014 through 7 June 2014
ER -