Abstraction for Falsification

Abstraction is traditionally used in the process of

verification

. There, an abstraction of a concrete system is sound if properties of the abstract system also hold in the concrete system. Specifically, if an abstract state

a

satisfies a property

ψ

then

all

the concrete states that correspond to

a

satisfy

ψ

too. Since the ideal goal of proving a system correct involves many obstacles, the primary use of formal methods nowadays is

falsification

. There, as in

testing

, the goal is to detect errors, rather than to prove correctness. In the falsification setting, we can say that an abstraction is sound if errors of the abstract system exist also in the concrete system. Specifically, if an abstract state

a

violates a property

ψ

, then

there exists

a concrete state that corresponds to

a

and violates

ψ

too.

An abstraction that is sound for falsification need not be sound for verification. This suggests that existing frameworks for abstraction for verification may be too restrictive when used for falsification, and that a new framework is needed in order to take advantage of the weaker definition of soundness in the falsification setting.

We present such a framework, show that it is indeed stronger (than other abstraction frameworks designed for verification), demonstrate that it can be made even stronger by parameterizing its transitions by predicates, and describe how it can be used for falsification of branching-time and linear-time temporal properties, as well as for generating testing goals for a concrete system by reasoning about its abstraction.