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.
https://hal.inria.fr/inria-00516025 Contributor : Hai WanConnect 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
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⟩