A case study on different modelling approaches based on model checking - verifying numerous versions of the alternating bit protocol with SMV

Recently, outstanding results have been achieved in the formal
verification of concurrent systems by model checking techniques. In
this paper we report our experience with SMV, a symbolic model
verifier, applied to a communication protocol, the alternating bit
protocol. We investigated different approaches of modeling the
alternating bit protocol in SMV. We describe the problems
encountered because of the restrictions of SMV. As a consequence, we
call for a more general language for model checking, which both
overcomes these disadvantages of SMV and enhances the possibility of
optimizations, and more specific input languages on top of it,
easing the application of model checking for the end user.