Making Components Fit: SPINing

The more popular it is to build an application from reusable software components, the more desperate is the need for showing correctness of such a composition. This requires on one hand, being able to formally specify behavior of software components, while, on the other hand, providing appropriate tool support for verification of correctness of the composition. In this paper, we suggest use of the formalism of Extended Behavior Protocols and present a tool chain for verification of composition correctness of component applications. The advantage of the proposed approach is using a well-tested and supported model checker Spin as a backend. As a proof of the concept, we share our experience with application of the method.