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

5 Citations (Scopus)

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
Volume2017-August
ISBN (Electronic)9781509067800
DOIs
StatePublished - Jan 12 2018
Event13th IEEE Conference on Automation Science and Engineering, CASE 2017 - Xi'an, China
Duration: Aug 20 2017Aug 23 2017

Other

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

Fingerprint

Temporal logic
Specifications

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Cite this

Dokhanchi, A., Yaghoubi, S., Hoxha, B., & Fainekos, G. (2018). Vacuity aware falsification for MTL request-response specifications. In 2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017 (Vol. 2017-August, pp. 1332-1337). IEEE Computer Society. https://doi.org/10.1109/COASE.2017.8256286

Vacuity aware falsification for MTL request-response specifications. / Dokhanchi, Adel; Yaghoubi, Shakiba; Hoxha, Bardh; Fainekos, Georgios.

2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017. Vol. 2017-August IEEE Computer Society, 2018. p. 1332-1337.

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

Dokhanchi, A, Yaghoubi, S, Hoxha, B & Fainekos, G 2018, Vacuity aware falsification for MTL request-response specifications. in 2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017. vol. 2017-August, IEEE Computer Society, pp. 1332-1337, 13th IEEE Conference on Automation Science and Engineering, CASE 2017, Xi'an, China, 8/20/17. https://doi.org/10.1109/COASE.2017.8256286
Dokhanchi A, Yaghoubi S, Hoxha B, Fainekos G. Vacuity aware falsification for MTL request-response specifications. In 2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017. Vol. 2017-August. IEEE Computer Society. 2018. p. 1332-1337 https://doi.org/10.1109/COASE.2017.8256286
Dokhanchi, Adel ; Yaghoubi, Shakiba ; Hoxha, Bardh ; Fainekos, Georgios. / Vacuity aware falsification for MTL request-response specifications. 2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017. Vol. 2017-August IEEE Computer Society, 2018. pp. 1332-1337
@inproceedings{c45b9abf39074fff951bd042be04a2b6,
title = "Vacuity aware falsification for MTL request-response specifications",
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.",
author = "Adel Dokhanchi and Shakiba Yaghoubi and Bardh Hoxha and Georgios Fainekos",
year = "2018",
month = "1",
day = "12",
doi = "10.1109/COASE.2017.8256286",
language = "English (US)",
volume = "2017-August",
pages = "1332--1337",
booktitle = "2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017",
publisher = "IEEE Computer Society",

}

TY - GEN

T1 - Vacuity aware falsification for MTL request-response specifications

AU - Dokhanchi, Adel

AU - Yaghoubi, Shakiba

AU - Hoxha, Bardh

AU - Fainekos, Georgios

PY - 2018/1/12

Y1 - 2018/1/12

N2 - 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.

AB - 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.

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

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

U2 - 10.1109/COASE.2017.8256286

DO - 10.1109/COASE.2017.8256286

M3 - Conference contribution

AN - SCOPUS:85044963940

VL - 2017-August

SP - 1332

EP - 1337

BT - 2017 13th IEEE Conference on Automation Science and Engineering, CASE 2017

PB - IEEE Computer Society

ER -