Loading...

Integrating module checking and deduction in a formal proof for the perlman Spanning Tree Protocol (STP)

Hojjat, H ; Sharif University of Technology | 2007

264 Viewed
  1. Type of Document: Article
  2. DOI: 10.3217/jucs-013-13-2076
  3. Publisher: 2007
  4. Abstract:
  5. 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. © J.UCS
  6. Keywords:
  7. Spanning Tree Protocol (STP) ; Module checking ; Deduction ; Formal proof ; Rebeca ; Formal verification ; Network protocols ; Modular verification
  8. Source: Journal of Universal Computer Science ; Volume 13, Issue 13 , 2007 , Pages 2076-2104 ; 0958695X (ISSN)
  9. URL: http://www.jucs.org/jucs_13_13/integrating_module_checking_and