What are the limits of model checking methods for the verification of real life protocols?

Model checking is a well known method to carry out formal verification of distributed systems. This method needs a model representing the behaviour of the system to be verified. The size of this model depends on the complexity of the system. To be able to verify real life systems, it is necessary to use techniques allowing to take advantage of all the available storage space, to reduce the amount of information needed for the verification and to speed up computation time. But the expressiveness of the languages used to describe the system and its expected behaviours (properties) limit the possible reductions. We present in this paper our choices for an automatic verification tool by using model checking. The preliminary results obtained from its use for the verification of a real life protocol allow us to make some estimations about the limits of model checking methods.