Formal Specification of Spanning Tree Protocol Using ACP

被引：2

作者：

Juan Roig, Pedro ^{[1
]}

Alcaraz, Salvador ^{[1
]}

Gilly, Katja ^{[1
]}

机构：

[1] Miguel Hernandez Univ, Dept Phys & Comp Architecture, Avda Univ S-N, Elche 03202, Alicante, Spain

来源：

ELEKTRONIKA IR ELEKTROTECHNIKA | 2017年 / 23卷 / 02期

关键词：

ACP; distributed algorithms; formal protocol specification; STP; VERIFICATION; NETWORKS;

D O I：

10.5755/j01.eie.23.2.18005

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Spanning-Tree Protocol (STP) has nowadays been implemented by most manufacturers in order to avoid loops in bridged networks. IEEE 802.1D STP is the original standard and it is run as a distributed algorithm by every bridge. In this paper we propose a formal specification of that STP by using a Process Algebra named Algebra of Communicating Processes (ACP), following a manual approach. Furthermore, STP protocol verification has been performed, both in a formal and in an informal way.

引用

页码：84 / 91

页数：8

共 15 条

[1]

[Anonymous], 1994, INF TECHN OP SYST IN

[2]

[Anonymous], 2004, 8021D2004 IEEE, P1

[3]

BERGSTRA JA, 1986, LECT NOTES COMPUT SC, V215, P9

[4] Design and analysis of dynamic leader election protocols in broadcast networks [J].