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.
Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1061124Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1551
 Edmund M. Clarke,Jr., Orna Grumberg and Doron A. Peled , Model Checking, The MIT press, 1999
 D.Harel, Statecharts: A Visual Formalism for Complex Systems, Science Computer Programming 8, pp 231-274, 1987
 Z.Manna, A.Pnueli, "The Temporal Logic of Reactive and Concurrent Systems," Springer Verlag, New York, 1992
 Valmari,A.: The State explosion Problem, Lectures on Petri Nets I:Basic Models, LNCS 1491, Springer- Verlag (1998) 429-528
 Alan B. Johnston, "Understanding the Session Initiation Protocol" Second edition, Artech house, ISBN 1-58053-655-7, 2004
 XML Metadata Interchange, http://www.omg.org/technology/documents/ formal/xmi.htm,visited on 17/10/2008
 BOUML An open source UML modeling tool, available at: http://sourceforge.net/project/, visited on 17/10/2008.
 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
 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.
 Gerard J. Holzmann, "The Model Checker Spin", IEEE Trans. on Software Engineering, Vol. 23, No. 5, (1997),279-295
 Kenneth L. Mc. Millan, "Symbolic Model Checking: An approach to the state explosion problem", Ph.D thesis submitted to Carnegie Mellon University (CMU), 1992
 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.