Probabilistic temporal logic falsification of cyber-physical systems

Houssam Abbas, Georgios Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

Research output: Contribution to journalArticle

49 Citations (Scopus)

Abstract

We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

Original languageEnglish (US)
Article number95
JournalTransactions on Embedded Computing Systems
Volume12
Issue number2 SUPPL.
DOIs
StatePublished - May 2013

Fingerprint

Temporal logic
Large scale systems
Trajectories
Sampling
Testing
Experiments
Cyber Physical System

Keywords

  • Hybrid systems
  • Metric temporal logic
  • Robustness
  • Testing

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software

Cite this

Probabilistic temporal logic falsification of cyber-physical systems. / Abbas, Houssam; Fainekos, Georgios; Sankaranarayanan, Sriram; Ivancic, Franjo; Gupta, Aarti.

In: Transactions on Embedded Computing Systems, Vol. 12, No. 2 SUPPL., 95, 05.2013.

Research output: Contribution to journalArticle

Abbas, Houssam ; Fainekos, Georgios ; Sankaranarayanan, Sriram ; Ivancic, Franjo ; Gupta, Aarti. / Probabilistic temporal logic falsification of cyber-physical systems. In: Transactions on Embedded Computing Systems. 2013 ; Vol. 12, No. 2 SUPPL.
@article{6fc4394869524c56ba42f663fa50c889,
title = "Probabilistic temporal logic falsification of cyber-physical systems",
abstract = "We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.",
keywords = "Hybrid systems, Metric temporal logic, Robustness, Testing",
author = "Houssam Abbas and Georgios Fainekos and Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta",
year = "2013",
month = "5",
doi = "10.1145/2465787.2465797",
language = "English (US)",
volume = "12",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "2 SUPPL.",

}

TY - JOUR

T1 - Probabilistic temporal logic falsification of cyber-physical systems

AU - Abbas, Houssam

AU - Fainekos, Georgios

AU - Sankaranarayanan, Sriram

AU - Ivancic, Franjo

AU - Gupta, Aarti

PY - 2013/5

Y1 - 2013/5

N2 - We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

AB - We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

KW - Hybrid systems

KW - Metric temporal logic

KW - Robustness

KW - Testing

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

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

U2 - 10.1145/2465787.2465797

DO - 10.1145/2465787.2465797

M3 - Article

VL - 12

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 2 SUPPL.

M1 - 95

ER -