Model Checking of Component Behavior Specification: A Real Life Experience

Abstract:

This paper is based on a real-life experience with behavior specification of a non-trivial component-based application. The experience is that model checking of such a specification yields very long error traces (providing counterexamples) in the order of magnitude of hundreds of states. Analyzing and interpreting such an error trace to localize and debug the actual specification is a tedious work. We present two techniques designed to address the problem: state space visualization and protocol annotation and share the positive experience with applying them, in terms of making the debugging process more efficient.

BibTeX:

@article{jezek_model_2006,
    title = {{Model Checking of Component Behavior Specification: A Real Life Experience}},
    author = {Ježek, Pavel and Kofroň , Jan and Plášil, František},
    year = {2006},
    journal = {{Electronic Notes in Theoretical Computer Science}},
    series = {{Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005)}},
    doi = {10.1016/j.entcs.2006.05.023},
    issn = {1571-0661},
    pages = {197--210},
    url = {http://www.sciencedirect.com/science/article/pii/S1571066106003859},
    volume = {160},
    shorttitle = {Model Checking of Component Behavior Specification},
}

Journal article