Vacuity aware falsification for MTL request-response specifications

Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos

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

12 Scopus citations

Abstract

We propose a method to improve the automated test case generation for Metric Temporal Logic (MTL) falsification for Cyber-Physical Systems (CPS). In this work, we focus on request-response MTL specifications. That is, specifications that consist of at least one antecedent and a corresponding consequent. Test case generation is particularly difficult for these specifications since the consequent is only considered if the antecedent is satisfied. Therefore, we propose a method that first targets the antecedent in the specification. We show that our framework can improve upon existing falsification methods on a number of benchmark problems.

Original languageEnglish (US)
Title of host publication2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017
PublisherIEEE Computer Society
Pages1332-1337
Number of pages6
ISBN (Electronic)9781509067800
DOIs
StatePublished - Jul 1 2017
Event13th IEEE Conference on Automation Science and Engineering, CASE 2017 - Xi'an, China
Duration: Aug 20 2017Aug 23 2017

Publication series

NameIEEE International Conference on Automation Science and Engineering
Volume2017-August
ISSN (Print)2161-8070
ISSN (Electronic)2161-8089

Other

Other13th IEEE Conference on Automation Science and Engineering, CASE 2017
Country/TerritoryChina
CityXi'an
Period8/20/178/23/17

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Vacuity aware falsification for MTL request-response specifications'. Together they form a unique fingerprint.

Cite this