Checking Software Component Behavior Using Behavior Protocols and Spin

Abstract:

Using software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols [11] are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela [7], which is consequently used as the input for the Spin model checker [7]. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components.

BibTeX:

@inproceedings{kofron_checking_2007,
    title = {{Checking Software Component Behavior Using Behavior Protocols and Spin}},
    author = {Kofroň, Jan},
    year = {2007},
    booktitle = {{Proceedings SAC 2007}},
    publisher = {ACM},
    series = {{SAC '07}},
    location = {New York, NY, USA},
    doi = {10.1145/1244002.1244326},
    isbn = {978-1-59593-480-2},
    pages = {1513--1517},
    url = {http://doi.acm.org/10.1145/1244002.1244326},
}

Proceedings paper