S.: Simulation and verification of a dynamic online auction

This paper deals with the formal specification, simulation and model-checking verification of an agent-based online auction. The need to understand dynamic behavior in auc-tions is increasing with the popularization of Internet auc-tions. This provides a strong motivation for the simulation of these complex systems. Since the auction interaction protocol is not trivial, it is suitable to use formal methods to ensure its correct functioning. Therefore, we investigate on the applicability of well-established techniques and tools from distributed systems, such as the formal specification language LOTOS, to specify and verify properties of inter-action protocols in multiagent systems, and simulate their behavior before the implementation