首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP)
  • 作者:Hossein Hojjat ; Hootan Nakhost ; Marjan Sirjani
  • 期刊名称:Journal of Universal Computer Science
  • 印刷版ISSN:0948-6968
  • 出版年度:2007
  • 卷号:13
  • 期号:13
  • 页码:2076-2104
  • 出版社:Graz University of Technology and Know-Center
  • 摘要:In the IEEE 802.1D standard for the Media Access Control layer (MAC layer) bridges, there is an STP (Spanning Tree Protocol) definition, based on the algorithm that was proposed by Radia Perlman. In this paper, we give a formal proof for correctness of the STP algorithm by showing that finally a single node is selected as the root of the tree and the loops are eliminated correctly. We use formal inductive reasoning to establish these requirements. In order to ensure that the bridges behave correctly regardless of the topology of the surrounding bridges and LANs, the Rebeca modular verification techniques are applied. These techniques are shown to be efficiently applicable in model checking of open systems.
Loading...
联系我们|关于我们|网站声明
国家哲学社会科学文献中心版权所有