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
Contributeur : Hai Wan
<>
Soumis le : dimanche 13 mars 2011 - 07:00:16
Dernière modification le : mardi 17 avril 2018 - 11:34:16
Document(s) archivé(s) le : mardi 14 juin 2011 - 02:21:38
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〉
