Formal specification and verification of JXTA´s Endpoint Routing Protocol

Author

Konga, Yannick L Kala ; Djouani, Karim

Author_Institution

Dept. of Electr. Eng., Tshwane Univ. of Technol., Tshwane, South Africa

fYear

2011

fDate

13-15 Sept. 2011

Firstpage

1

Lastpage

7

Abstract

JXTA protocols describe a framework for peer-to-peer networking, independent of underlying transport protocols, for peer collaboration and message exchange. The JXTA project is an open source initiative and its protocols are informally specified as exchanges of XML-based messages between entities. This paper presents the formal specification and automated verification of the one JXTA´s core protocol: the Endpoint Routing Protocol. This protocol runs at the core of the JXTA architecture is responsible for routing messages between peers. The PROMELA based formal specification serves as input to the SPIN model checker to prove the protocol´s incompleteness through the presence of deadlocks and live-locks.

Keywords

formal specification; formal verification; groupware; peer-to-peer computing; routing protocols; transport protocols; JXTA protocols; PROMELA; endpoint routing protocol; formal specification; formal verification; message exchange; peer collaboration; peer-to-peer networking; transport protocols; Formal specifications; Formal verification; Peer to peer computing; Reliability; Routing; Routing protocols; JXTA; formal specification; formal verification; model checking; peer-to-peer; routing protocol;

fLanguage

English

Publisher

ieee

Conference_Titel

AFRICON, 2011

Conference_Location

Livingstone

ISSN

2153-0025

Print_ISBN

978-1-61284-992-8

Type

conf

DOI

10.1109/AFRCON.2011.6072086

Filename

6072086