Specification and verification of a multi-agent coordination protocol with TLA+

被引：1

作者：

Arbs Paiva, Pedro Yuri ^{[1
]}

Saotome, Osamu ^{[1
]}

Brandauer, Christof ^{[2
]}

机构：

[1] ITA, Div Engn Eletron, Sao Jose Dos Campos, Brazil

[2] Salzburg Res Forsch Gesell, Adv Network Ctr, Salzburg, Austria

来源：

2018 VIII BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEMS ENGINEERING (SBESC 2018) | 2018年

关键词：

TLA(+); Industrial Control Systems; Formal Methods; Model Checking; Coordination; Security;

D O I：

10.1109/SBESC.2018.00039

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

There is a general rule which says that about 50 percent of the elapsed time in a project is expended in testing. Finding bugs in software might be an awkward task, especially when there are design errors. The common sense, however, frequently has a biased view of formal methods, associating it with high complexity and low return on investment. That would supposedly be worth only for critical parts of a system. TLA(+) is a formal specification language that is based on first-order logic and set theory. In this paper, we describe how we used it to formally specify a coordination protocol and how we applied model checking technique to verify correctness properties. We also discuss the advantages of TLA(+) and the relatively low overhead to get used to it.

引用

页码：207 / 212

页数：6

共 50 条

[21] Coordination in multi-agent RoboCup teams [J].

Candea, C ;

Hu, HS ;

Iocchi, L ;

Nardi, D ;

Piaggio, M .

ROBOTICS AND AUTONOMOUS SYSTEMS, 2001, 36 (02) :67-86

[22] Behavioral modeling and verification of multi-agent systems for manufacturing control [J].

Yeung, W. L. .

EXPERT SYSTEMS WITH APPLICATIONS, 2011, 38 (11) :13555-13562

[23] Formal specification of holonic multi-agent systems framework [J].

Rodriguez, S ;

Hilaire, V ;

Koukam, A .

COMPUTATIONAL SCIENCE - ICCS 2005, PT 3, 2005, 3516 :719-726

[24] Formal Verification of Open Multi-Agent Systems [J].

Kouvaros, Panagiotis ;

Lomuscio, Alessio ;

Pirovano, Edoardo ;

Punchihewa, Hashan .

AAMAS '19: PROCEEDINGS OF THE 18TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS, 2019, :179-187

[25] Multi-agent Based Logistics Coordination System [J].

Wang, Yan-Ling .

MATERIALS SCIENCE AND INFORMATION TECHNOLOGY, PTS 1-8, 2012, 433-440 :3106-3111

[26] Evaluation of Multi-agent Coordination on Embedded Systems [J].

Menegol, Marcelo S. ;

Hubner, Jomi F. ;

Becker, Leandro B. .

ADVANCES IN PRACTICAL APPLICATIONS OF AGENTS, MULTI-AGENT SYSTEMS, AND COMPLEXITY: THE PAAMS COLLECTION, 2018, 10978 :212-223

[27] Specification and verification of a dynamic reconfiguration protocol for agent-based applications [J].

Cornejo, MA ;

Garavel, H ;

Mateescu, R ;

de Palma, N .

NEW DEVELOPMENTS IN DISTRIBUTED APPLICATIONS AND INTEROPERABLE SYSTEMS, 2001, 70 :229-242

[28] Rational verification: game-theoretic verification of multi-agent systems [J].

Abate, Alessandro ;

Gutierrez, Julian ;

Hammond, Lewis ;

Harrenstein, Paul ;

Kwiatkowska, Marta ;

Najib, Muhammad ;

Perelli, Giuseppe ;

Steeples, Thomas ;

Wooldridge, Michael .

APPLIED INTELLIGENCE, 2021, 51 (09) :6569-6584

[29] Rational verification: game-theoretic verification of multi-agent systems [J].

Alessandro Abate ;

Julian Gutierrez ;

Lewis Hammond ;

Paul Harrenstein ;

Marta Kwiatkowska ;

Muhammad Najib ;

Giuseppe Perelli ;

Thomas Steeples ;

Michael Wooldridge .

Applied Intelligence, 2021, 51 :6569-6584

[30] Multi-site coordination using a multi-agent system [J].

Monteiro, Thibaud ;

Roy, Daniel ;

Anciaux, Didier .

COMPUTERS IN INDUSTRY, 2007, 58 (04) :367-377

← 1 2 3 4 5 →