Specification and verification of a dynamic reconfiguration protocol for agent-based applications

被引：0

作者：

Cornejo, MA ^{[1
]}

Garavel, H ^{[1
]}

Mateescu, R ^{[1
]}

de Palma, N ^{[1
]}

机构：

[1] INRIA Rhone Alpes, F-38330 Montbonnot St Martin, France

来源：

NEW DEVELOPMENTS IN DISTRIBUTED APPLICATIONS AND INTEROPERABLE SYSTEMS | 2001年 / 70卷

关键词：

compositional verification; distributed application; dynamic reconfiguration; LOTOS; mobile agent; model-checking; specification;

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Dynamic reconfiguration increases the availability of distributed applications by allowing them to evolve at run-time. This paper deals with the formal specification and model-checking verification of a dynamic reconfiguration protocol used in industrial agent-based applications. Starting from a reference implementation in JAVA, we produced a specification of the protocol using the Formal Description Technique LOTOS. We also specified a set of temporal logic formulas characterizing the correct behaviour of each protocol primitive. Finally, we studied various finite state configurations of the protocol, on which we verified these requirements using the CADP protocol engineering tool set.

引用

页码：229 / 242

页数：14

共 25 条

[1]

BELLISSARD L, 1999, P SRDS 99 LAUS SUISS

[2]

BLOOM T, 1993, SOFTWARE ENG J, V8, P102, DOI 10.1049/sej.1993.0014

[3]

Clarke E, 2001, Model checking

[4] INTRODUCTION TO ALGEBRAIC SPECIFICATIONS BASED ON THE LANGUAGE ACT ONE [J].

DEMEER, J ;

ROTH, R ;

VUONG, S .

COMPUTER NETWORKS AND ISDN SYSTEMS, 1992, 23 (05) :363-392

[5]

DEPALMA N, 2000, C3DS PUBL TECH REPOR

[6]

DEPALMA N, 1999, P ERSADS 99 MAD ISL

[7]

EMERSON EA, P LICS 86, P267

[8]

FERNANDEZ JC, 1996, LECT NOTES COMPUTER, V1102, P437

[9]

FERNANDEZ JC, 1996, LECT NOTES COMPUTER, V1102, P348

[10]

GARAVEL H, 2001, P FORTE 01 CHEJ ISL

← 1 2 3 →