Enabling Automatic Certification of Online Auctions

Wei Bai
Emmanuel M. Tadjouddine
Yu Guo

We consider the problem of building up trust in a network of online auctions by software agents. This requires agents to have a deeper understanding of auction mechanisms and be able to verify desirable properties of a given mechanism. We have shown how these mechanisms can be formalised as semantic web services in OWL-S, a good enough expressive machine-readable formalism enabling software agents, to discover, invoke, and execute a web service. We have also used abstract interpretation to translate the auction's specifications from OWL-S, based on description logic, to COQ, based on typed lambda calculus, in order to enable automatic verification of desirable properties of the auction by the software agents. For this language translation, we have discussed the syntactic transformation as well as the semantics connections between both concrete and abstract domains. This work contributes to the implementation of the vision of agent-mediated e-commerce systems.

In Bara Buhnova, Lucia Happe and Jan Kofroň: Proceedings 11th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2014), Grenoble, France, 12th April 2014, Electronic Proceedings in Theoretical Computer Science 147, pp. 123–132.
Published: 2nd April 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.147.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org