Sciweavers

Share
ICDCSW
2000
IEEE

Compositional Verification of a Third Generation Mobile Communication Protocol

10 years 8 months ago
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
Sari Leppänen, Matti Luukkainen
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ICDCSW
Authors Sari Leppänen, Matti Luukkainen
Comments (0)
books