Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Modelling and Verification of JXTA peer-topeer Network Protocols

    Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

    Tunis, Tunisia, 15-16 September 2011


    Yannick L Kala Konga, Karim Djouani and Guillaume Noel


    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.


    PDF filePDF Version of this Paper (665kb)