Towards model checking & simulation of a multi-tier negotiation protocol for service chains
Paul Karaenke, Stefan Kirn · Adaptive Agents and Multi-Agents Systems · 2010
The object of our research is resource allocation which considers contractual dependencies across service chain tiers to avoid overcommitment and overpurchasing. We propose a multi-tier negotiation protocol for solving this problem. The proposed artifact is developed from an interaction protocol engineering perspective and a protocol specification is given. Besides basic safety properties like the absence of deadlock, we formally verify that the protocol prevents overcommitments and overpurchasing by means of the model checker Spin.