Modelling IMPP : Please help

Dear Sirs,
Can someone please help me with the following:
I want to model and formally verfiy IMPP (as a part of course comm. protocol
engg).
I am using promella for modelling, and most probably spin for verifying.

I need some guidance on the important feutures to verify and model.

Till now i have followed the model described in RFC and aim to model mainly
the following features:
1. Two main services, Instant message and Presence.
2. some Presentities
3. Separate i/o channels for each presentity for interacting with the
presence and instant message service
4. The Presentity contains watcher also(of the the first type, fetcher)
.......

Verification properties:
1. Access control rules(rfc 2779 2.3)
2. subcriptions 5.1
3. message delivery
4. deadlocks, non reachable states etc....
......

Any suggesstions or feedback is most required.

thank you for the consideration ....

Regards,
Sohel.

p.s. Is any implementation of impp available in c++ or java.... ?




_______________________________________________
Sohel Khan
Research Assistant, Information and Computer Science, KFUPM, Dhahran 31261.
P.O Box : 1183
Homepage: http://www.ccse.kfupm.edu.sa/~sohel/
mailto:[email protected]  Phone
No(Res):00966-3-860-6536,(Off):00966-3-860-1490

" Truth is Simple "
_______________________________________________







  [reminder: [email protected] for non-technical discussions, please]