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

45 Scopus citations

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
Subtitle of host publicationComputation and Control
Pages125-134
Number of pages10
DOIs
StatePublished - May 10 2012
Event15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12 - Beijing, China
Duration: Apr 17 2012Apr 19 2012

Publication series

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

Conference

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

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

Fingerprint Dive into the research topics of 'Falsification of temporal properties of hybrid systems using the cross-entropy method'. Together they form a unique fingerprint.

  • 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). (HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control). https://doi.org/10.1145/2185632.2185653