Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS-NT and CADP

Abstract : Dynamic software systems that provide the ability to reconfigure themselves seem to be reaching a complexity that suggests the use of formal methods in the design process, helping system designers master that complexity, better understand their systems, find and correct bugs rapidly, and ultimately build strong confidence in the correctness of their systems. As an illustration of this trend, this paper reports on our experience with the co-design and specification of the reconfiguration protocol of a component-based platform, intended as the foundation for building robust dynamic systems. We wrote the specification in LOTOS-NT, whose evolution from the E-LOTOS standard proved especially suited to this work. We extensively verified the protocol using the CADP toolbox. This formal analysis helped to detect several issues which enabled us to correct various parts of the protocol. The protocol is implemented in the Synergy virtual machine, the prototype of an ongoing research programme on reconfigurable and robust component-aware virtual machines.
Type de document :
Communication dans un congrès
Springer. 17th International Symposium on Formal Methods (FM'11), Jun 2011, Limerick, Ireland. 6664, pp.103-117, 2011, LNCS. 〈10.1007/978-3-642-21437-0_10〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00648909
Contributeur : Gwen Salaün <>
Soumis le : mardi 6 décembre 2011 - 15:38:29
Dernière modification le : mercredi 11 avril 2018 - 01:56:11
Document(s) archivé(s) le : vendredi 16 novembre 2012 - 14:30:29

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Fabienne Boyer, Olivier Gruber, Gwen Salaün. Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS-NT and CADP. Springer. 17th International Symposium on Formal Methods (FM'11), Jun 2011, Limerick, Ireland. 6664, pp.103-117, 2011, LNCS. 〈10.1007/978-3-642-21437-0_10〉. 〈hal-00648909〉

Partager

Métriques

Consultations de la notice

410

Téléchargements de fichiers

120