Temporal logic falsification of cyber-physical systems: An input-signal-space optimization approach

Arend Aerts, Bryan Tong Minh, Mohammad Reza Mousavi, Michel A. Reniers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

Abstract

Temporal logic falsification is a promising approach to model-based testing of cyber-physical systems. It starts off with a formalized system requirement specified as a Metric Temporal Logic (MTL) property. Subsequently, test input signals are generated in order to stimulate the system and produce an output signal. Finally, output signals of the system under test are compared to those prescribed by the property to falsify the property by means of a counterexample. To find such a counterexample, Markov Chain Monte-Carlo (MCMC) methods are used to construct an optimization problem to steer the test input generations to those input areas that maximize the probability of falsifying the property. In this paper, we identify two practical issues in the above-mentioned falsification process. Firstly, a fixed time domain of the input-signal space is assumed in this process, which restricts the frequency content of the (generated) input signals. Secondly, the existing process allows for input selection steered by the distribution of a single input variable. We address these issues, by firstly, considering multiple time domains for input-signal space. Subsequently, an input-signal-space optimization problem is formally defined and implemented in S-TaLiRo+, an extension of S-TaLiRo (an existing implementation for solving the MTL falsification problem). Secondly, we propose a decoupled scheme that considers the distribution of each input variable independently. The applicability of the proposed solutions are experimentally evaluated on well-known benchmark problems.

Original languageEnglish
Title of host publication2018 IEEE 11th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2018
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Pages214-223
Number of pages10
ISBN (Electronic)978-1-5386-6352-3
DOIs
Publication statusPublished - 16 Jul 2018
Event11th IEEE International Conference on Software Testing Verification and Validation Workshops (ICSTW 2018) - Vasteras, Sweden
Duration: 9 Apr 201813 Apr 2018
Conference number: 11

Conference

Conference11th IEEE International Conference on Software Testing Verification and Validation Workshops (ICSTW 2018)
Abbreviated titleICSTW 2018
Country/TerritorySweden
CityVasteras
Period9/04/1813/04/18

Keywords

  • Cyber physical systems
  • Metric temporal logic
  • Model based testing
  • Temporal logic falsification

Fingerprint

Dive into the research topics of 'Temporal logic falsification of cyber-physical systems: An input-signal-space optimization approach'. Together they form a unique fingerprint.

Cite this