Advertisement

Validation of the Sessionless Mode of the HTTPR Protocol

  • Paolo Romano
  • Milton Romero
  • Bruno Ciciani
  • Francesco Quaglia
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)

Abstract.

Reliable delivery of messages using open and product-neutral protocols has been identified as a needed technology in enterprise computing and a fundamental middleware component in several E-Business systems. The HTTPR protocol aims at guaranteeing reliable message delivery, even in the presence of failures, by providing the sender with the ability to deliver a message once, and only once, to its intended receiver(s). This work reports the experience in the formalization and validation of the sessionless mode of the HTTPR protocol through the use of the SPIN model checker. To overcome the state space explosion problem that arose while validating the protocol, a decompositional approach was used which could be of general interest in the validation of complex systems.

Keywords

Client Side Network Failure Persistent Storage Crash Failure Receive Outcome 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Emerson, E.A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science (1990)Google Scholar
  2. 2.
    Hypertext Transfer Protocol – HTTP/1.1 (RFC), http://www.ietf.org/rfc/rfc2616.txt?number=2616
  3. 3.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)Google Scholar
  4. 4.
    Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. on Software Engineering (May 1997)Google Scholar
  5. 5.
  6. 6.
  7. 7.
  8. 8.
    Microsoft, Microsoft Message Queuing (MSMQ), http://www.microsoft.com/msmq
  9. 9.
    Oracle, Oracle Message Broker 1.0, Data Sheet (October 1999) Google Scholar
  10. 10.
    Romano, P., Romero, M., Ciciani, B., Quaglia, F.: Validation of the Sessionless Mode of the HTTPR Protocol, Tech. Rep. 12-03, DIS, University of Rome “La Sapienza”, http://ftp.dis.uniroma1.it/pub/quaglia/tr12-03.ps
  11. 11.
    Ruys, T., Langerak, R.: Validation of Bosch’ Mobile Communication Network Architecture with Spin. In: Proceedings of the 9th SPIN Workshop, Grenoble (2002) Google Scholar
  12. 12.
    Ruys, T.: SPIN Tutorial: how to become a SPIN Doctor. In: Proceedings of the 3th SPIN Workshop, Enschede (1997) Google Scholar
  13. 13.
    Spin Online References, Directives to Reduce Memory Use, http://spinroot.com/spin/Man/Pan.html#D4
  14. 14.
    Sun, Java Messaging System, http://java.sun.com/products/jms/
  15. 15.
    Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Proc. 5th Int. Conference on Computer Aided Verification, Elounda (1993)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Paolo Romano
    • 1
  • Milton Romero
    • 1
  • Bruno Ciciani
    • 1
  • Francesco Quaglia
    • 1
  1. 1.DISUniversità “La Sapienza”RomaItaly

Personalised recommendations