Modelling and Verification of JXTA peer-topeer Network Protocols

Recent advances in peer-to-peer computing have allowed its evolution as a reliable alternative to traditional centralised computing methods. The JXTA project is a popular open source describes a platform formed by six protocols purposed to enable interoperable, ubiquitous and reliable peer-topeer networking. We present a formal model of integrated JXTA protocols using Promela. We subsequently verify the model with the SPIN model-checker for internal consistency. Because the integrated model proves to be too large formal verification due its size and complexity, we verify the protocols separately. Number of non-progress cycles and an invalid end state are detected and we provide possible solutions approaches for these errors.