Title :
Modeling and verification of some communication protocols
Author :
Talukder, Kamrul Hasan ; Harada, Koichi
Author_Institution :
Graduate Sch. of Eng., Hiroshima Univ.
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;
Conference_Titel :
Advanced Communication Technology, 2006. ICACT 2006. The 8th International Conference
Conference_Location :
Phoenix Park
Print_ISBN :
89-5519-129-4
DOI :
10.1109/ICACT.2006.206434
