Formal verification of negotiation protocols for multi-agent manufacturing systems
International Journal of Production Research
Taylor & Francis
Agent based systems, agile manufacturing, process planning, simulation applications, software engineering
Formal verification is an important means of tackling behavioural problems such as deadlocks in multi-agent systems. This paper is concerned with the role played by formal verification in the simulation-based performance analysis of multi-agent manufacturing systems. A discrete-event simulation case study is presented to show how varying certain timing parameters of the agent negotiation protocol affects the performance of a multi-agent manufacturing system as well as the chance of getting deadlocks among the software agents. When one tries to determine the optimal values of these timing parameters based on the simulation results, formal verification can help refine the results by confirming whether deadlocks among software agents are indeed possible for particular parameter values. This involves modelling the system's real-time behaviour according to the simulation model and applying the techniques and tools of model checking.
Copyright © 2011 Taylor & Francis
Access to external full text or publisher's version may require subscription.
Yeung, W. L. (2011). Formal verification of negotiation protocols for multi-agentmanufacturing systems. International Journal of Production Research, 49(12), 3669-3690. doi: 10.1080/00207543.2010.492407