Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/inria-00516025
Contributor : Hai Wan Connect in order to contact the contributor
Submitted on : Sunday, March 13, 2011 - 7:00:16 AM
Last modification on : Thursday, February 3, 2022 - 11:16:42 AM
Long-term archiving on: : Tuesday, June 14, 2011 - 2:21:38 AM

File

Formal_Specification_and_Verif...
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

97

Files downloads

87