时间自动机与网络协议验证

摘要

随着网络协议复杂性的增大,其自身的潜在错误变得更加重要.使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误.时间自动机是形式化方法的一种,可以很好地应用于网络协议验证中.目前基于时间自动机已经开发出了多种自动验证工具.文章介绍了网络协议验证的几种方法,并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法.