JUCS - Journal of Universal Computer Science 13(13): 2076-2104, doi: 10.3217/jucs-013-13-2076
Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP)
expand article infoHossein Hojjat, Hootan Nakhost§, Marjan Sirjani|
‡ University of Tehran, Tehran, Iran§ Sharif University of Technology, Iran| Department of Electrical and Computer Engineering, University of Tehran, Iran
Open Access
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.
formal methods, network protocols, formal verification, Rebeca, modular verification