
Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification
Author(s) -
Johan Lidén Eddeland,
Seyed Ghassem Miremadi,
Knut Åkesson
Publication year - 2020
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/f4vs
Subject(s) - computer science , semantics (computer science) , solver , set (abstract data type) , benchmark (surveying) , theoretical computer science , programming language , statement (logic) , outcome (game theory) , model checking , mathematics , geodesy , mathematical economics , political science , law , geography
Temporal-logic based falsification of Cyber-Physical Systems is a testing technique used to verify certain behaviours in simulation models, however the problem statement typically requires some model-specific tuning of parameters to achieve optimal results. In this experience report, we investigate how different optimization solvers and objective functions affect the falsification outcome for a benchmark set of models and specifications. With data from the four different solvers and three different objective functions for the falsification problem, we see that choice of solver and objective function depends both on the model and the specification that are to be falsified. We also note that using a robust semantics of Signal Temporal Logic typically increases falsification performance compared to using Boolean semantics.