THE SAFETY AND LIVENESS PROPERTIES OF THE NETWORK PROTOCOL BASED ON TLA

摘要：

　　We propose a definition of the class of all fairness properties of concurrent systems.In this work,we introduce to the fair transition system,and then discuss the relation among safety property,liveness property and fairness property in the temporal logic of actions.On the way,we give a recent overview work on fairness in reactive and concurrent systems,and innovatively prove the relation among of the fairness.Furthermore,we consider a ring-based leader election protocol.Leader election is an important protocol in distributed computing.We have proven or verified that this protocol satisfies safety and liveness properties,and use the temporal logic of actions for formalization and specification.

关键词： Safety Liveness Fairness TLA Leader election protocol

作者: Junming Zhang Shigong Long Kouwu Wang

作者单位: Science college,Guizhou university,Guiyang,550025,China College of Computer Science and information,Guizhou university,Guiyang,550025,China, College of Computer Science and information,Guizhou university,Guiyang,550025,China

会议类型: 国际会议

会议名称: 2013IET International Conference on Information and Communication Technologies(IETICT2013)2013IET信息与通信技术国际会议

会议地点: 北京

会议语种:英文

页码: 164-168

在线出版日期: 2013-04-27（万方平台首次上网日期，不代表论文的发表时间）