M. Tech. Electrical Engineering. / This research presented an integrated formal model of the JXTA protocol suite. The integrated model is constructed from the individual models describing the behaviours of protocols entities. Written in the PROMELA specification language, the finite state automata of these models are shown instead. The SPIN-based formal verification revealed that this studys integrated model was too large to perform for the computational resources available. This was in spite of the application of multiple complexity reduction techniques. Subsequently, as final recourse, the research resorted to the formal verification of individual protocols by making further abstraction of the interaction and dependencies between protocols. A number of errors were found including an invalid end state in the routing protocols and multiple non-progress cycles.