Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches

Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo

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

8 Citations (Scopus)


Falsification of hybrid systems is attracting ever-growing attention in quality assurance of Cyber-Physical Systems (CPS) as a practical alternative to exhaustive formal verification. In falsification, one searches for a falsifying input that drives a given black-box model to output an undesired signal. In this paper, we identify input constraints—such as the constraint “the throttle and brake pedals should not be pressed simultaneously” for an automotive powertrain model—as a key factor for the practical value of falsification methods. We propose three approaches for systematically addressing input constraints in optimization-based falsification, two among which come from the lexicographic method studied in the context of constrained multi-objective optimization. Our experiments show the approaches’ effectiveness.

Original languageEnglish
Title of host publicationNASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
Number of pages19
ISBN (Print)9783030557539
Publication statusPublished - 2020
Externally publishedYes
Event12th International Symposium on NASA Formal Methods, NFM 2020 - Moffett Field, United States
Duration: May 11 2020May 15 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12229 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Symposium on NASA Formal Methods, NFM 2020
Country/TerritoryUnited States
CityMoffett Field

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches'. Together they form a unique fingerprint.

Cite this