Falsification of temporal properties of hybrid systems using the cross-entropy method

Sriram Sankaranarayanan, Georgios Fainekos

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

42 Citations (Scopus)

Abstract

Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right input distributions in order to expose corner-case violations. However, this is also known to be a hard problem, in practice. In this paper, we present an application of the cross-entropy method for adaptively choosing input distributions for falsifying temporal logic properties of hybrid systems. We present various choices for representing input distribution families for the cross-entropy method, ranging from a complete partitioning of the input space into cells to a factored distribution of the input using graphical models. Finally, we experimentally compare the falsification approach using the cross-entropy method to other stochastic and heuristic optimization techniques implemented inside the tool S-Taliro over a set of benchmark systems. The performance of the cross entropy method is quite promising. We find that sampling inputs using the cross-entropy method guided by trace robustness can discover violations faster, and more consistently than the other competing methods considered.

Original languageEnglish (US)
Title of host publicationHSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control
Pages125-134
Number of pages10
DOIs
StatePublished - 2012
Event15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12 - Beijing, China
Duration: Apr 17 2012Apr 19 2012

Other

Other15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12
CountryChina
CityBeijing
Period4/17/124/19/12

Fingerprint

Hybrid systems
Entropy
Temporal logic
Embedded systems
Systems analysis
Sampling
Testing

Keywords

  • Cross-entropy method
  • Hybrid systems
  • Metric temporal logic
  • Monte- carlo simulation
  • Robustness
  • Testing

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Cite this

Sankaranarayanan, S., & Fainekos, G. (2012). Falsification of temporal properties of hybrid systems using the cross-entropy method. In HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control (pp. 125-134) https://doi.org/10.1145/2185632.2185653

Falsification of temporal properties of hybrid systems using the cross-entropy method. / Sankaranarayanan, Sriram; Fainekos, Georgios.

HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. 2012. p. 125-134.

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

Sankaranarayanan, S & Fainekos, G 2012, Falsification of temporal properties of hybrid systems using the cross-entropy method. in HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. pp. 125-134, 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12, Beijing, China, 4/17/12. https://doi.org/10.1145/2185632.2185653
Sankaranarayanan S, Fainekos G. Falsification of temporal properties of hybrid systems using the cross-entropy method. In HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. 2012. p. 125-134 https://doi.org/10.1145/2185632.2185653
Sankaranarayanan, Sriram ; Fainekos, Georgios. / Falsification of temporal properties of hybrid systems using the cross-entropy method. HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control. 2012. pp. 125-134
@inproceedings{10e54cdaefed4c3c8fdcc62d1e154969,
title = "Falsification of temporal properties of hybrid systems using the cross-entropy method",
abstract = "Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right input distributions in order to expose corner-case violations. However, this is also known to be a hard problem, in practice. In this paper, we present an application of the cross-entropy method for adaptively choosing input distributions for falsifying temporal logic properties of hybrid systems. We present various choices for representing input distribution families for the cross-entropy method, ranging from a complete partitioning of the input space into cells to a factored distribution of the input using graphical models. Finally, we experimentally compare the falsification approach using the cross-entropy method to other stochastic and heuristic optimization techniques implemented inside the tool S-Taliro over a set of benchmark systems. The performance of the cross entropy method is quite promising. We find that sampling inputs using the cross-entropy method guided by trace robustness can discover violations faster, and more consistently than the other competing methods considered.",
keywords = "Cross-entropy method, Hybrid systems, Metric temporal logic, Monte- carlo simulation, Robustness, Testing",
author = "Sriram Sankaranarayanan and Georgios Fainekos",
year = "2012",
doi = "10.1145/2185632.2185653",
language = "English (US)",
isbn = "9781450312202",
pages = "125--134",
booktitle = "HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control",

}

TY - GEN

T1 - Falsification of temporal properties of hybrid systems using the cross-entropy method

AU - Sankaranarayanan, Sriram

AU - Fainekos, Georgios

PY - 2012

Y1 - 2012

N2 - Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right input distributions in order to expose corner-case violations. However, this is also known to be a hard problem, in practice. In this paper, we present an application of the cross-entropy method for adaptively choosing input distributions for falsifying temporal logic properties of hybrid systems. We present various choices for representing input distribution families for the cross-entropy method, ranging from a complete partitioning of the input space into cells to a factored distribution of the input using graphical models. Finally, we experimentally compare the falsification approach using the cross-entropy method to other stochastic and heuristic optimization techniques implemented inside the tool S-Taliro over a set of benchmark systems. The performance of the cross entropy method is quite promising. We find that sampling inputs using the cross-entropy method guided by trace robustness can discover violations faster, and more consistently than the other competing methods considered.

AB - Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right input distributions in order to expose corner-case violations. However, this is also known to be a hard problem, in practice. In this paper, we present an application of the cross-entropy method for adaptively choosing input distributions for falsifying temporal logic properties of hybrid systems. We present various choices for representing input distribution families for the cross-entropy method, ranging from a complete partitioning of the input space into cells to a factored distribution of the input using graphical models. Finally, we experimentally compare the falsification approach using the cross-entropy method to other stochastic and heuristic optimization techniques implemented inside the tool S-Taliro over a set of benchmark systems. The performance of the cross entropy method is quite promising. We find that sampling inputs using the cross-entropy method guided by trace robustness can discover violations faster, and more consistently than the other competing methods considered.

KW - Cross-entropy method

KW - Hybrid systems

KW - Metric temporal logic

KW - Monte- carlo simulation

KW - Robustness

KW - Testing

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

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

U2 - 10.1145/2185632.2185653

DO - 10.1145/2185632.2185653

M3 - Conference contribution

SN - 9781450312202

SP - 125

EP - 134

BT - HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control

ER -