论文部分内容阅读
该文提出了一种新的混合型形式描述方法、以保证协议形式描述具备适用性，易证性和易懂性。该方法采用了有限状态机、语义学及抽象数据型等技术。首先，作者用有限状态机对协议系统控制部分进行描述，并给出了正确性证明方法；对于状态转换，采用了语义学的定义方法，避免了程序设计语言自身的限制；最后，用抽象数据型的概念描述了数据类型，如帧格式等，弥补了以上两种技术的不足。利用以上形式描述方法，给出了Ethernet协议的形式描述。（本刊录）