Enhancing Temporal Logic Falsification With Specification Transformation and Valued Booleans

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 article, 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.

I. Introduction

Assuring the quality of cyber-physical systems (CPSs) is an important task that is growing more and more complex. Industrial-size systems with both discrete and continuous dynamics, i.e., hybrid systems, require durable methods for design automation [1], as well as validation methods that are beyond the current capabilities of, e.g., model-checking [2]. Since the general problem of finding the set of reachable states for this kind of systems is undecidable [3], we instead resort to testing the systems. For testing and/or monitoring of CPSs, there are many possible approaches (see [4], [5] for two surveys)—in this article, we consider falsification of temporal logic specifications. Another approach is deductive methods for proving properties of CPSs [6], but in many industrial applications there is no mathematical model to analyze, instead there is only the possibility to simulate the system under test. Falsification can be done for CPSs both with the actual hardware, or as in the case of this article, where the hardware is being simulated.