论文部分内容阅读
本文建立了用于表述含有无限值状态成分的通讯协议机的抽象模型，给出了基于该模型的形式检证法，试制了检证系统．该检证法不需要假定信道的有界性．对于给定的通信协议，检证系统将判定其对指定状态的可到达性．做为检证例，从ＯＳＩ参照模型中抽出了大同步点设置功能单位，就“无死锁”、“无传输错误”等性质进行了实际检证
In this paper, an abstract model of communication protocols for describing state components with infinite states is established, and a formal verification method based on this model is given. The verification method does not need to assume the boundedness of the channel. For a given communication protocol, the verification system will determine its reachability to the specified state. As a test case, from the OSI reference model out of a large synchronization point set functional units, on the “no deadlock”, “no transmission error” and other properties of the actual test