Formal verification of negotiation protocols for multi-agent manufacturing systems
Document Type
Journal article
Source Publication
International Journal of Production Research
Publication Date
1-1-2011
Volume
49
Issue
12
First Page
3669
Last Page
3690
Publisher
Taylor & Francis
Keywords
Agent based systems, agile manufacturing, process planning, simulation applications, software engineering
Abstract
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.
DOI
10.1080/00207543.2010.492407
Print ISSN
00207543
E-ISSN
1366588X
Publisher Statement
Copyright © 2011 Taylor & Francis
Access to external full text or publisher's version may require subscription.
Full-text Version
Publisher’s Version
Language
English
Recommended Citation
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