Verification of protocol design using UML - SMV

Simple item page
dc.contributor.authorPrashanth, C.M.
dc.contributor.authorChandrashekar Shet, K.
dc.date.accessioned2026-02-05T09:36:30Z
dc.date.issued2009
dc.description.abstractIn 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.
dc.identifier.citationWorld Academy of Science, Engineering and Technology, 2009, 36, , pp. 544-548
dc.identifier.issn2010376X
dc.identifier.urihttps://idr.nitk.ac.in/handle/123456789/27553
dc.subjectAutomatic verification
dc.subjectIndustry standards
dc.subjectObjectoriented modeling
dc.subjectProtocol design
dc.subjectProtocol model
dc.subjectSession initiation protocol
dc.subjectSoftware systems
dc.subjectState charts
dc.subjectSupporting tool
dc.subjectUML Model
dc.subjectUML statechart diagrams
dc.subjectDesign
dc.subjectInternet protocols
dc.subjectModel checking
dc.subjectSemantics
dc.subjectVerification
dc.subjectUnified Modeling Language
dc.titleVerification of protocol design using UML - SMV

Files

Collections

Journal Articles