Vacuity Aware Falsification for MTL Request-Response Specifications

被引：0

作者：

Dokhanchi, Adel ^{[1
]}

Yaghoubi, Shakiba ^{[1
]}

Hoxha, Bardh ^{[2
]}

Fainekos, Georgios ^{[1
]}

机构：

[1] Arizona State Univ, Sch Comp Informat & Decis Syst Engn, Tempe, AZ 85281 USA

[2] Southern Illinois Univ, Dept Comp Sci, Carbondale, IL USA

来源：

2017 13TH IEEE CONFERENCE ON AUTOMATION SCIENCE AND ENGINEERING (CASE) | 2017年

关键词：

VERIFICATION; ROBUSTNESS; SYSTEMS;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：1332 / 1337

页数：6