Validation of the Sessionless Mode of the HTTPR Protocol

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.