Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans

TL;DR

This paper improves the falsification process for cyber-physical systems by transforming specifications into Signal Temporal Logic and employing Valued Booleans with additive robust semantics, enhancing scalability and effectiveness.

Contribution

It introduces a specification transformation framework and applies Valued Booleans with additive robust semantics to improve falsification in large-scale CPS verification.

Findings

Additive robust semantics outperform traditional methods on certain benchmarks.

Specification transformation enables better handling of complex CPS models.

Performance varies depending on model and specification characteristics.

Abstract

Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this paper, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into Signal Temporal Logic. The second addition is the use of Valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.