Publication at Faculty of Mathematics and Physics, Central Library of Charles University |
2005
Abstract
Model checking of a nontrivial component-based application yields very long error traces. We present two techniques designed to address the problem of localization and debugging the actual specification: state space visualization and protocol annotation.