148 articles – 162 Notices  [english version]

inria-00516025, version 1

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

Hai Wan () 1, Ming Gu a, 1, Xiaoyu Song b, 1

Mathematical and Computer Modelling 50, 7-8 (2009)

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.

  • a –  School of Software, Tsinghua University
  • b –  ECE Dept, Portland State University
  • 1 :  FORMES (LIAMA)
  • INRIA – Tsinghua University / Beijing – LIAMA
  • Domaine : Informatique/Systèmes embarqués
 
  • inria-00516025, version 1
  • http://hal.inria.fr/inria-00516025
  • oai:hal.inria.fr:inria-00516025
  • Contributeur : Hai Wan <>
  • Soumis le : Dimanche 13 Mars 2011, 07:00:16
  • Dernière modification le : Dimanche 13 Mars 2011, 07:00:16