HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications

Manuel Aguilar Cornejo 1 Hubert Garavel 1 Radu Mateescu 1 Noël de Palma 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072397
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 9:51:10 AM
Last modification on : Friday, February 4, 2022 - 3:12:05 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:05:52 PM

Identifiers

  • HAL Id : inria-00072397, version 1

Citation

Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, Noël de Palma. Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. [Research Report] RR-4222, INRIA. 2001. ⟨inria-00072397⟩

Share

Metrics

Record views

108

Files downloads

227