University of Regina (CANADA)
CADP (Construction and Analysis of Distributed Processes)
1575 lines of LOTOS (14 data types / 23 sorts, 6 processes)
3,228,732 states and 10,733,000 transitions
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.
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
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),
Available from our FTP 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 our FTP site in PDF or PostScript
Dr. Samira Sadaoui-Mouhoub
Department of Computer Science
University of Regina
3737 Wascana Parkway
Regina, SK S4S 0A2
Tel: +1 306-337-2340
Fax: +1 306-585-4745
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|