Towards Model Checking & Simulation of a Multi-Tier Negotiation Protocol for Service Chains (Extended Abstract)
Paul Karaenke, Stefan Kirn · 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.