Compositional Verification of a Third Generation Mobile Communication Protocol

Model-checking has turned out to be an efficient and relatively easy-to-use technique in the 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

• Type: Conference
• Year: 2000
• Where: ICDCSW
• Authors: Sari Leppänen, Matti Luukkainen
• Keywords: Behavior Model, Behavior Model Generation, Computer Networks, ICDCSW 2000, State Explosion