Modeling and verifying business interactions via commitments and dialogue actions

Abstract

A variety of business interactions in open environments can be captured in terms of creation and manipulation of social commitments among the agents. Such interactions include B2B and B2C processes and contracts as realized via web services and other technologies. Also, the interaction protocols are formulated in terms of commitments to regulate agents' behaviors. However, such protocols can benefit from a stronger treatment of flexible interactions via dialogue actions to capture a rich variety of real-life business scenarios. This paper addresses the challenges of modeling and verifying business interactions using commitments and actions on such commitments augmented with dialogue actions to reconcile conflicts and reason about the validity of such commitments. We introduce the NetBill protocol taken from e-business domain to demonstrate the specification of a new class of formal protocols for agent negotiation. Finally, we use the MCMAS symbolic model checker to automatically verify this protocol against some given properties. We present the implementation and experimental results of this protocol and its verification. © 2010 Springer-Verlag.