Compositional Verification of a Third Generation
Mobile Communication Protocol
Sari Leppanen* and Matti Luukkainen**
* Nokia Research Center, FINLAND
** University of Helsinki, FINLAND
Abstract
Model-checking has shown to be an efficient and relatively easy-to-use
technique in verification of formally described programs. However, there
is one major drawback in using model-checking: the state explosion, i.e.,
the behavior models of real-life programs tend to be extremely large. In the
article it is shown how the theories of behavioral equivalences with a
compositional style of behavior model generation can alleviate the state
explosion in verifying the externally observable properties of SDL
descriptions. The practical usability of the method is evidenced
with a case study that is taken from ongoing development of third
generation mobile communication systems.
Keywords:
Formal verification, model-checking , Compositional methods, SDL,
Communication protocols, UMTS