Behavior Protocol Verification: Fighting State Explosion

Abstrakt

A typical problem formal verification faces is the size of the model of a system being verified. Even for a small system, the state space of the model tends to grow exponentially (state explosion).

In this paper, we present a new representation of state spaces suitable for implementing operations upon behavior protocols of software components. The proposed representation is linear in length of the source behavior protocol.

By trading space for time, it allows handling behavior protocols of 'practical size'. As a proof of concept, two versions of a verification tool based on the proposed technique are discussed.