Addressing State Explosion in Behavior Protocol Verification

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 [1]. 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, a verification tool for behavior protocols is discussed.

• Type: Conference
• Year: 2004
• Where: SNPD
• Authors: Martin Mach, Frantisek Plasil
• Keywords: Behavior Protocols, Problem Formal Verification, SNPD 2004, SNPD 2007, State Spaces