Verification of Protocol Design using UML - SMV

Authors: Prashanth C.M., K. Chandrashekar Shet

Abstract:

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.

Keywords: Unified Modeling Language, Statechart, Verification, Protocol Design, Model Checking.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1061124

References:

[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.