inria-00516025, version 1
Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
Mathematical and Computer Modelling 50, 7-8 (2009)
- a – School of Software, Tsinghua University
- b – ECE Dept, Portland State University
- 1 :
-
http://liama.ia.ac.cn/wiki/projects:formes:home
INRIA – Tsinghua University / Beijing – LIAMA Tsinghua University FIT Building Haidian District 100084 Beijing China Chine
Références bibliographiques
- Type de publication : Articles dans des revues avec comité de lecture
- Domaine : Informatique/Systèmes embarqués
- Titre : Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
- Résumé : 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.
- Langue du document : Anglais
- Titre de la revue :
Mathematical and Computer Modelling Publisher Elsevier ISSN 0895-7177 - Date de publication : 2009
- Audience : internationale
- Editeur commercial : Elsevier
- Volume : 50
- Numéro : 7-8
- DOI : 10.1016/j.mcm.2009.06.001
- Projet ANR :
Référence du projet ANR-08-BLAN-0326-01 Année 2009 Acronyme du projet SIVES Titre du projet A Simulation and Verification based platform for developing Embedded Systems
Liste des fichiers attachés à ce document :
- inria-00516025, version 1
- http://hal.inria.fr/inria-00516025
- oai:hal.inria.fr:inria-00516025
- Contributeur :
- Soumis le : Dimanche 13 Mars 2011, 07:00:16
- Dernière modification le : Dimanche 13 Mars 2011, 07:00:16
Documents associés
Exporter