Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections

Hai Wan 1 Ming Gu 1 Xiaoyu Song 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : The paper presents a formal modeling and analysis of a protocol for narrow bandwidth channels of service connection establishment and termination. The protocol is characterized by state traces and formally verified by a theorem proving system PVS. Relevant properties are specified and verified in terms of inductive principles. The effectiveness of the proposed method is evidenced by the elaborate analysis which unveils a subtle bug in the initial protocol implementation. The approach is scalable for an arbitrary number of agents.
Type de document :
Article dans une revue
Mathematical and Computer Modelling, Elsevier, 2009, 50 (7-8), 〈10.1016/j.mcm.2009.06.001〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00516025
Contributeur : Hai Wan <>
Soumis le : dimanche 13 mars 2011 - 07:00:16
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : mardi 14 juin 2011 - 02:21:38

Fichier

Formal_Specification_and_Verif...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Hai Wan, Ming Gu, Xiaoyu Song. Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections. Mathematical and Computer Modelling, Elsevier, 2009, 50 (7-8), 〈10.1016/j.mcm.2009.06.001〉. 〈inria-00516025〉

Partager

Métriques

Consultations de la notice

138

Téléchargements de fichiers

66