Hybrid System Falsification under (In)equality Constraints via Search Space Transformation

Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo

Research output: Contribution to journalArticlepeer-review

Abstract

The verification of hybrid systems is intrinsically hard, due to the continuous dynamics that leads to infinite search spaces. Therefore, research attempts focused on hybrid system falsification of a black-box model, a technique that aims at finding an input signal violating the desired temporal specification. Main falsification approaches are based on stochastic hill-climbing optimization, that tries to minimize the degree of satisfaction of the temporal specification, given by its robust semantics. However, in the presence of constraints between the inputs, these methods become less effective. In this article, we solve this problem using a search space transformation that first maps points of the unconstrained search space to points of the constrained one, and then defines the fitness of the former ones based on the robustness values of the latter ones. Based on this search space transformation, we propose a falsification approach that performs the search over the unconstrained space, guided by the robustness of the mapped points in the constrained space. We introduce three versions of the proposed approach that differ in the way of selecting the mapped points. Experiments show that the proposed approach outperforms state-of-the-art constrained falsification approaches.

Original languageEnglish
Article number9211466
Pages (from-to)3674-3685
Number of pages12
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume39
Issue number11
DOIs
Publication statusPublished - Nov 2020
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Hybrid System Falsification under (In)equality Constraints via Search Space Transformation'. Together they form a unique fingerprint.

Cite this