Agent-Based Dynamic Online Auction Protocol.

Organisation:	University of Regina (CANADA)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Mobile Agents.
Period:	2003
Size:	1575 lines of LOTOS (14 data types / 23 sorts, 6 processes) 3,228,732 states and 10,733,000 transitions
Description:	Internet auction protocols are complex multiagent systems whose dynamic behaviour must be well-understood. This case-study deals with the formal modelling, simulation and verification of the English Auction Interaction Protocol defined by FIPA (Foundation for Intelligent Physical Agents). In this protocol, the bidding is open, the duration is fixed, the bidding price increases gradually, and a single winner (or no one) is chosen at the end of the auction. The auction process consists of 13 different steps, and involves several types of agents: administrator, auctioneer, seller, and buyers. Agents communicate by asynchronous point-to-point message passing, according to an event-reaction scheme. The communication infrastructure uses the Message Transport Service (MTS) based on the FIPA Agent Communication Language (ACL). MTS ensures the transfer, addressing, and buffering of messages, and also the error handling. In order to enable its formal analysis, the English online auction protocol was specified in LOTOS. The configuration considered consists of one administrator, one auctioneer, one seller, and two buyer agents. Several data types were used to represent the different entities involved in communication (agents and sets of agents, session identifiers, and various message kinds). An abstraction of the communication infrastructure was modelled as a single LOTOS process, which transfers messages and stores them in local buffers associated to individual agents. The architecture of the protocol follows the resource-oriented LOTOS specification style, whereas software agents are modelled using the state-oriented style. The auction specification supports the subscription and unsubscription of a buyer at any time during the auction; however, the current winner is not allowed to cancel his/her subscription. This LOTOS specification was subsequently analyzed using the tools provided by CADP. After inspecting the protocol behaviour by means of interactive simulation, the tools EXHIBITOR and TGV were respectively used to produce scenarios and test cases matching different goals, such as auction failures. In addition, 7 correctness properties of the auction protocol (5 safety properties and 2 liveness properties) were identified, formulated in regular alternation-free mu-calculus, and verified on the LOTOS specification using EVALUATOR.
Conclusions:	This case-study assessed that LOTOS is suitable for designing interaction protocols for multiagent systems, and that standard validation and verification technologies such as those implemented in CADP can be successfully used to analyze these protocols. The LOTOS specification developed for the English auction interaction protocol can be generalized to handle any interaction protocol in multiagent systems.
Publications:	[Chen-Sadaoui-03] Bo Chen and Samira Sadaoui. "Simulation and Verification of a Dynamic Online Auction". Proceedings of the 7th IASTED International Conference on Software Engineering and Applications SEA'2003 (Marina del Rey, CA, USA), November 2003. Available from the CADP Web site in PDF or PostScript [Chen-Sadaoui-05] Bo Chen and Samira Sadaoui. "A Generic Formal Framework for Multiagent Interaction Protocols". International Journal of Software Engineering and Knowledge Engineering, Volume 15(1), pp. 61-86, February 2005. Preliminary version available on-line at: http://www.cs.uregina.ca/Research/Techreports/2003-05.pdf or from the CADP Web site in PDF or PostScript
Contact:	Dr. Samira Sadaoui-Mouhoub Assistant Professor Department of Computer Science University of Regina 3737 Wascana Parkway Regina, SK S4S 0A2 Canada Office: CW308.14 Tel: +1 306-337-2340 Fax: +1 306-585-4745 E-mail: sadaouis@cs.uregina.ca
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page