Verification of Protocol Design using UML - SMV

In recent past, the Unified Modeling Language (UML) has become the de facto industry standard for object-oriented modeling of the software systems. The syntax and semantics rich UML has encouraged industry to develop several supporting tools including those capable of generating deployable product (code) from the UML models. As a consequence, ensuring the correctness of the model/design has become challenging and extremely important task. In this paper, we present an approach for automatic verification of protocol model/design. As a case study, Session Initiation Protocol (SIP) design is verified for the property, “the CALLER will not converse with the CALLEE before the connection is established between them ". The SIP is modeled using UML statechart diagrams and the desired properties are expressed in temporal logic. Our prototype verifier “UML-SMV" is used to carry out the verification. We subjected an erroneous SIP model to the UML-SMV, the verifier could successfully detect the error (in 76.26ms) and generate the error trace.

• Prashanth C.M.
• K. Chandrashekar Shet

• Unified Modeling Language
• Statechart
• Verification
• Protocol Design
• Model Checking.

[1] Edmund M. Clarke,Jr., Orna Grumberg and Doron A. Peled , Model
Checking, The MIT press, 1999
[2] D.Harel, Statecharts: A Visual Formalism for Complex Systems, Science
Computer Programming 8, pp 231-274, 1987
[3] Z.Manna, A.Pnueli, "The Temporal Logic of Reactive and Concurrent
Systems," Springer Verlag, New York, 1992
[4] Valmari,A.: The State explosion Problem, Lectures on Petri Nets I:Basic
Models, LNCS 1491, Springer- Verlag (1998) 429-528
[5] Alan B. Johnston, "Understanding the Session Initiation Protocol" Second
edition, Artech house, ISBN 1-58053-655-7, 2004
[6] XML Metadata Interchange, http://www.omg.org/technology/documents/
formal/xmi.htm,visited on 17/10/2008
[7] BOUML An open source UML modeling tool, available at:
http://sourceforge.net/project/, visited on 17/10/2008.
[8] Alan J. Hu, M. Fujita, Chris Wilson, "Formal verification of HAL S1
system Cache coherence Protocol". In proceedings of Int. conference on
computer design, IEEE, 1997
[9] T. Y.C. Woo, Simon S. lam, "Design, Verification and Implementation
of Authentication Protocol", In proc. of Int. conference on Network
protocols, pp 81-90, 1994.
[10] Gerard J. Holzmann, "The Model Checker Spin", IEEE Trans. on
Software Engineering, Vol. 23, No. 5, (1997),279-295
[11] Kenneth L. Mc. Millan, "Symbolic Model Checking: An approach to
the state explosion problem", Ph.D thesis submitted to Carnegie Mellon
University (CMU), 1992
[12] I. Beer, S. Ben-David, C. Eisner and Landvar," RuleBase an industryoriented
formal verification tool", Proceedings of 33rd Design Automation
Conference (DAC), Association for Computing Machinery
Inc.,(1996), 655-660.