Formal specification and verification of JXTA´s Endpoint Routing Protocol

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.