论文部分内容阅读
基于形式化方法的协议一致性测试是确保协议可靠性的基本手段。当前,一些新型互联网协议中存在不同的并行组件,而传统形式化方法难以描述这些特点,本文针对基于扩展并行多组件状态机的网络协议测试进行了深入的研究。本文综述了相关的研究现状,指出单一组件模型难以描述多组件的协议,而现有的多组件模型也难以描述组件间共享数据的情况;软件定义网络是带有并行多组件的新型互联网协议的典型代表,但尚缺少采用形式化方法的黑盒测试。本文研究了扩展并行多组件状态机的建模框架,分别提出了三种不同的扩展并行多组件状态机模型:为了描述并行组件间采用共享数据通信的情况,提出了读取外部变量的并行扩展有限状态机模型;为了描述多级流水线结构,提出了流水线扩展有限状态机模型,其同级组件间存在共享变量读写,跨级组件间存在单向消息传递;将消息传递与网络拓扑结合,提出了信息表扩展有限状态机模型。本文提出了基于定义使用路径的并行扩展有限状态机测试生成方法。首先生成内部变量的定义使用路径,然后使其可执行化并生成外部变量的定义使用路径。该方法是启发式方法,可用于变量无限取值的模型并避免状态空间爆炸。本文提出了基于可达图的并行扩展有限状态机层次化测试生成方法。该方法适用于变量取值有限的模型,其使用自底向上的可达图生成缓解状态空间爆炸,同时使用自顶向下的测试序列生成确保可执行。将前述两种测试生成方法分别应用于源地址验证协议测试,验证了方法的有效性。本文提出了流水线扩展有限状态机测试生成方法。首先将模型转换为数据图并找到数据路径;然后生成数据路径上的组件状态机的前导序列并组成测试序列。通过实验对比表明该方法能够生成系统覆盖模型的测试集,并有效控制了测试生成的时间和空间开销。将本方法应用于Open Flow交换机的一致性测试,发现了协议实现中的错误和协议中值得讨论的问题。本文提出了信息表扩展有限状态机测试生成方法。对于设计缺陷,用模型检测工具根据模型生成反例;对于实现错误,综合运用组件部分组合、拓扑对称化简和拓扑模拟执行生成扩展测试序列。该方法能够同时检测设计缺陷和实现错误,而且在与网络拓扑结合的同时,减缓状态空间爆炸的风险。