Modeling and verification of some communication protocols

Author

Talukder, Kamrul Hasan ; Harada, Koichi

Author_Institution

Graduate Sch. of Eng., Hiroshima Univ.

Volume

3

fYear

2006

fDate

20-22 Feb. 2006

Lastpage

2198

Abstract

This paper presents a technique of modeling and verification of some communication protocols for remote procedure call (RPC). These protocols include request (R) protocol, request reply (RR) protocol and request-reply-acknowledgement (RRA) protocol. The above-mentioned protocols are modeled in symbolic model verifier (SMV), a formal verification tool. In modeling of each protocol, each of the two agents (client and server) is modeled as a finite state machine. The common channel between these agents is modeled as a bounded queue of message. The verification results of some important features of these protocols verified by SMV are also presented

Keywords

finite state machines; program verification; protocols; remote procedure calls; communication protocols; finite state machine; formal verification tool; remote procedure call; request reply protocol; request-reply-acknowledgement protocol; symbolic model verifier; Circuit simulation; Circuit testing; Computer errors; Electronic mail; Formal verification; Hardware; Performance evaluation; Programming profession; Protocols; System testing; Modeling; R protocol; RR protocol; RRA protocol; Remote Procedure Call (RPC); Verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Advanced Communication Technology, 2006. ICACT 2006. The 8th International Conference

Conference_Location

Phoenix Park

Print_ISBN

89-5519-129-4

Type

conf

DOI

10.1109/ICACT.2006.206434

Filename

1626039