Return to search

Formal specification and verification of peer-to-peer network protocols.

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.

Identiferoai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:tut/oai:encore.tut.ac.za:d1000638
Date January 2011
CreatorsKonga, Yannick Lokombo Kala.
ContributorsDjouani, K. (Karim), Noel, G.
Source SetsSouth African National ETD Portal
LanguageEnglish
Detected LanguageEnglish
TypeText
FormatPDF

Page generated in 0.0021 seconds