一种新的通信协议分析方法（发布于1987年）

本文提出一种用于协议分析的新方法，它以本文提出的带有参数计数器的有限状态自动机为基础，对协议模型进行可达性分析。这种方法不仅解决了“状态爆炸问题”，并有利于实现自动验证。由所生成的可达树，可以构成马尔可夫链模型，并由此确定协议的性能。文中讨论了马尔可夫链模型的性质与建立过程，并进行了吸收分析。最后，给出了简单分组传输协议的例子，以说明方法的应用。