Behavior Protocols Verification: Fighting State Explosion

Abstract:

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, two versions of a verification tool based on the proposed technique are discussed.

BibTeX:

@article{mach_behavior_2005,
    title = {{Behavior Protocols Verification: Fighting State Explosion}},
    author = {Mach, Martin and Plášil, Františ ek and Kofroň, Jan},
    year = {2005},
    journal = {{International Journal of Computer and Information Science}},
    number = {1},
    issn = {1525-9293},
    pages = {22--30},
    url = {https://www.semanticscholar.org/paper/Behavior-Protocols-Verification-\%3A-Fighting-State-Mach-Plasil/07450736bfcd18a475eabd1a07bc997d1fcb45ac},
    volume = {6},
    shorttitle = {Behavior Protocols Verification},
}

Journal article