Formal Verification of the IEEE 802.1D Spanning Tree Protocol Using Extended Rebeca

The STP (Spanning Tree Protocol) which is standardized as IEEE 802.1D has been used in many bridges and switches of networks. This algorithm tries to eliminate loops in bridged networks. In this study the correctness of STP algorithm is formally verified using Extended Rebeca. In order to not to be confined to a specific case or set of cases we used a compositional verification approach. This allows us to gain generality in verifying the algorithm. The clarity and convenience in model checking by means of Extended Rebeca suggests that this language can be used for verifying more network protocols in future.