Abstract
In complex software component systems, it is desirable to verify the correctness of the composition before deployment. To achieve a trustworthy composition, the behavior of components is formally described and the composition is verified against communication errors.
Unfortunately, the number of states of a model tends to grow exponentially with the size of the model's description --- the state explosion problem. Because the exhaustive verification has to visit all the states of the model, the verification leads to unacceptable space and time requirements. In this thesis, we present several approaches to cope with the state explosion problem in behavior protocols.
First, we reduce a size of the specification by enhancing the specification language by exceptions and, additionally, we reduce the specification by symbolic manipulations with respect to composition. Then, we present a novel approach to distributed verification, which involves external storage devices.
Finally, we reduce the number of stat