Abstraction in program model checking

Question

Explain the term Abstraction in program model checking and how it is distingush with data abstraction?

Answer 1

Introduction:

Abstraction is essential for software verification. Without abstraction, a realistic software application is usually too large to be analyzed exhaustively with a model checker. Abstraction aims to transform a program into another program that still has some key properties of the original program, but is much simpler, and therefore easier to analyze. In model checking, abstractions are used to reduce the size of a program’s state space in an attempt to overcome the memory limitations of model-checking algorithms.

Given a program and a property, the strategy of model checking by abstraction can be summarized as follows.

1. Define an abstraction mapping between the concrete program and an abstract program.

2. Use the abstraction mapping to transform the concrete program into an abstract program; usually the property needs also to be transformed into an abstract property.

3. Apply model checking on the abstract program.

4. Map the results of model checking the abstract program back to the original program.

We distinguish between data abstractions, which replace the large domains of program variables with smaller domains, and control abstractions, such as slicing, which remove program components that are irrelevant to the property under analysis. This chapter is mainly concerned with data abstraction. Abstractions can be further characterized by the way they preserve a property or class of properties being verified, or by the way they approximate the behavior of the system being verified.