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 o 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 cold be of general interest in the validation of complex systems.
展开▼
