利用“协议机退缩”的通信协议形式检证  

COMMUNICATION PROTOCOL VERIFICATION VIA DEGENERATION

作　　者：邵峰晶[1] 刘遵仁[1] 孙孝瑞[1] 

机构地区：[1]青岛大学理工学院计算机系

出　　处：《青岛大学学报（自然科学版）》1997年第1期26-38,共13页Journal of Qingdao University(Natural Science Edition)

摘　　要：针对提供高优先度通信协议其检证时生成协议机状态数庞大，使检证难以进行的问题，本文给出了协议机的退缩检证法．通过将给定协议机的检证问题转换为若干个较小协议机的相应检证问题，简化了协议形式检证的复杂性．利用退缩检证法及已建立的检证系统，证明了假设无信道错误时ＯＳＩ参照模型中会话层协议的主要部分，满足“无死锁”、“无传输错误”Communicating finite state machines is the useful abstract model for specifying and verifying communication protocols. If the boundedness of the communication channels is guaranted, many important verification problems are decidable. Unfortunately, the channel boundedness is itself undecidable, and many practical protocols do not satisfy channel boundedness. This paper presents a method without assuming channel boundedness to verify some properties such as eventuality for a class of protocols modeled as two communicating finite state machines. A verificating system based on our method has been implemented to decide whether an eventuality property is satisfied for a given protocol. Another method is investigated for decreasing the complexity of verification, degeneration of a protocol. For some parts of the OSI session protocol, it has been verified by using the verfication system that neither protocol error nor deadlock occurs unless a transmission error occurs. The effect of the degeneration of a protocol is also discussed by using the example.

关 键 词：OSI 计算机通信 协议机 通信协议 退缩检验 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]