Formal verification of negotiation protocols for multi-agent manufacturing systems

Wing Lok YEUNG

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

2 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)3669-3690
Number of pages22
JournalInternational Journal of Production Research
Volume49
Issue number12
DOIs
Publication statusPublished - 1 Jan 2011

Fingerprint

Software agents
Network protocols
Discrete event simulation
Model checking
Real time systems
Multi agent systems
Formal verification
Negotiation protocol
Manufacturing systems
Deadlock
Simulation
Modeling
Simulation model
Multi-agent systems
Performance analysis

Keywords

  • Agent based systems
  • agile manufacturing
  • process planning
  • simulation applications
  • software engineering

Cite this

@article{347535e65ff74f6cbd4d9e80f38b4ac4,
title = "Formal verification of negotiation protocols for multi-agent manufacturing systems",
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.",
keywords = "Agent based systems, agile manufacturing, process planning, simulation applications, software engineering",
author = "YEUNG, {Wing Lok}",
year = "2011",
month = "1",
day = "1",
doi = "10.1080/00207543.2010.492407",
language = "English",
volume = "49",
pages = "3669--3690",
journal = "International Journal of Production Research",
issn = "0020-7543",
publisher = "Taylor and Francis Ltd.",
number = "12",

}

Formal verification of negotiation protocols for multi-agent manufacturing systems. / YEUNG, Wing Lok.

In: International Journal of Production Research, Vol. 49, No. 12, 01.01.2011, p. 3669-3690.

Research output: Journal PublicationsJournal Article (refereed)Researchpeer-review

TY - JOUR

T1 - Formal verification of negotiation protocols for multi-agent manufacturing systems

AU - YEUNG, Wing Lok

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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.

AB - 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.

KW - Agent based systems

KW - agile manufacturing

KW - process planning

KW - simulation applications

KW - software engineering

UR - http://commons.ln.edu.hk/sw_master/178

U2 - 10.1080/00207543.2010.492407

DO - 10.1080/00207543.2010.492407

M3 - Journal Article (refereed)

VL - 49

SP - 3669

EP - 3690

JO - International Journal of Production Research

JF - International Journal of Production Research

SN - 0020-7543

IS - 12

ER -