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

随着计算机网络与通信技术的发展，网络协议的复杂性 也日益增加。协议开发的难度增大、周期增长，而且潜在错 误增多。而协议中的每一处错误和缺陷都将给网络系统的稳 定性、可靠性等带来巨大的危害。用形式化的方法来描述与 验证网络协议可以发现协议中潜在的错误。时间自动机可以 用直观的形式描述网络协议，特别是其中的时间特性。现在 已经开发出了基于时间自动机的多种验证工具，都可以很好 地用于网络协议验证中。