软件。这个模糊测试构架包括被测的控制软件，网络测试平台，还有一个选择输入序列，驱使测试平台，周期性检测不变量的集中orchestrator（协调器）。
我们不使用这样的QA测试平台，而是搭建我们自己的。我们的测试平台模仿在轻量软件交换机和主机的网络设备的控制平面行为（以便支持最小数据平面的转发）。然后我们在模仿网络上层运行控制软件，连接交换机和控制器。模仿网络管理来自单一地址的事件的运行，这样就允许它记录下一系列的事件顺序。这个设计类似QA测试平台，Figure3具体解释了过程。
我们不同于别的设计特点是：模拟平台干预了所有的信道，允许延迟或者丢掉消息来减少在实际异步网络中可能见到的失败模式。
我们使用模拟网络来发现控制软件的漏洞。最常见的，我们基于指定的事件发生的可能性生成随机输入序列，然后在网络状态下周期性地检查不变量。我们也循环运行模拟网络以便我们可以检查网络的状态，进行手动引出我们认为可能触发故障的事件顺序。 ? 执行最小化（Performing Minimization）：
发现一个不变量违例之后，我们调用delta debugging 来最小化记录的路径。我们使用测试基础构架本身来复制每一个中间子序列。在复制过程中，模拟网络迫使事件顺序按照需要去保持原始的happens-before 关系，通过利用插入信息信道来管理顺序（功能等价的），然后等直到合适的时间去插入输入。例如，如果最初路径包括了一个链路故障，这个链路故障是先于消息中心到达的，在复制过程中，模拟网络等待直到它观察到一个等价功能的ping探针抵达，然后批准探针通过，告知转发器去中断这条链路。 ? 与现存的测试平台的整合
在设计STS时，我们打算利用现存的QA测试基础构架来执行这项技术。我们尝试避免在测试平台下关于语言和指令的提前假设。 ? 应对不确定性
并行执行中的不确定性来自于系统响应返回值、处理顺序决定以及异步信号传达的不同。这些不确定性的来源会影响STS是否能够复制违例在复制过程中。
我们尝试去提升的QA测试构架不能够减轻不确定性。但STS的应对不确定性的主要途径就是多次复制每个子序列。比如，一个不确定的故障出现的概率是p,我们可以对概率建模——在r次复制后我们可以观测到这个故障发生的概率为: 1-(1-p)^r 这个指数公式很好的验证了我们的结果。例如，即使一个原始的故障仅仅被20%的复制序列所触发，那么我们在中间处不会触发故障的概率约为1%如果我们对每个子序列复制20次。Figure 5向我们展示了多次复制对于减轻不确定性影响的效果，可以清晰地得出：随着每个子序列中复制列的最大数量的增加，最终的得到的最小因果序列的也会越小，意味着STS对网络故障的自动诊断效果越好。
6. 对STS的评价测试：
评估的方法论：
? 在5中开源的SDN控制平台上进行模糊测试，这5中平台分别是ONOS (Java)，POX (Python)，
NOX(C++)， Pyretic(Python)， Floodlight(Java)。得到了7种新的故障。
? 最小限度的量化人为操作造成的故障。通过为之前已知的人为的故障寻找MCSes的方式来说明STS平
台运行良好与否的边界。
? 我们最终的目的是减少花费在故障诊断上的时间。然而这个时间是很难去测量的，因为这取决于不同开
发人员的技术水平以及对代码基础的熟悉程度，因此，我们采取一种定量的方法展示STS最小化记录L的能力以及定性的使用MCS的方法去诊断新发现的故障。
综合的评价测试结果：
?
STS可以大大减少最初路径输入事件数量，并且把输入事件序列减少为“最小因果序列”，通过运行时间那一栏，我们可以发现尽管一个对系统的语言、指令不熟悉的开发人员，STS可以把大部分的故障自动诊断处理时间控制在30分钟以内。
? NoD（Network Optimized Datalog）
1. 背景
当前存在的网络诊断工具缺少一个通用的规范说明语言和网络模型的硬编码。因此，这些工具有很大的缺陷性，例如它们不能够对抽象度高的策略进行建模，也不能对动态网络进行建模。标准的网络诊断工具（如Model Checkers）配备了有表达力的规范说明和模型语言，但是它们又不能够衡量大的头文件空间。
因此，引入了“网络优化数据日志”工具（Network Optimized Datalog）作为一个网络诊断工具，它的规范说明语言和建模语言都是Datalog。
2. 目标
NoD工具允许在动态网络里检查关于网络可达性策略的“信条（Beliefs）”。一个“信条”是一个网络工程师认为正确的高层次的不变量（例如：“网络控制器不能够访问网络”）。“信条”可能不可靠，但是检查这些“信条”可以用很少的人工力气发现那些故障或者异常策略。被驳斥的“信条”也可以用作改进的信条的基础。此外，NoD允许网络分析师去塑造一个动态网络通过添加新的Datalog规则。
我们的目标是发现尽量多的故障通过静态检查路由转发表和ACLs（访问控制列表）而不用等待故障去触发昂贵的现场事件。在我们的操作网络中，我们大约观测到一个顾客可见的超过一个小时的操作停断故障占了四分之一的主要性质；去诊断这些现场事件是十分昂贵的，并且减少了收入降低了顾客的满意度。随着商业服务的部署，用静态检查来诊断故障变得十分重要。
这篇论文的作者已经在他们公司的公共云（云服务的一种）部署了第一版本的故障诊断检测器，并且它也可以规律性的检查出来一些故障。但是当前的故障诊断工具有着两个著名的障碍：
?
缺少了解：确定要到底要检查什么规范是主要的障碍。可达性策略可以被自然的想成“谁到了谁那里”的问题。如何利用存在的网络诊断技术去处理问题当检查人员都不了解整个被诊断的网络。 ?
网络churn：现存的网络诊断技术假设了网络是静态的，而且在转发状态的静态截图上进行操作。但是实际上，许多的网络故障发生在当网络第一次被展开时候的扩建。现存的诊断工具如Antreater，VeriFlow， Hassel等等都是假设一个固定的转发规则和固定的流量包头，而没有对出现的错误甚至头文件发生改变的建模。 NoD去克服这两种问题的回答： ? ?
用通用的规范说明语言去规范“信条”。 用通用的建模语言去建模网络。
3. 方法：
? 数据日志模型（Datalog Model）
首先明确一个理想的网络规范建模语言应该满足以下五个特点： ? ? ? ? ?
可以提供所有的解决方案：我们想要找到所有的可以到达B的A中的数据包头。 数据包重写功能 一个大的头空间 通用的规范说明语言 通用的网络建模语言
数据日志模型可以满足1,4,5条功能，对于2,3功能该模型可能很难实现，在稍后的NoD方法中将会满足2,3。
注意到在语言层面上，NoD就是一种数据日志。下面是一个关于Datalog语言的简单的例子
为了找到所有的从离开A可以到达B的数据包，我们提出了Datalog问题？A(dst,src)放在所有的路由器转发规则后面。
? 用Datalog语言去编码“信条（beliefs）”
?
保护集
考虑一个下面的信条：结构管理是不可达的对于客户虚拟机。 具体用Datalog语言编码如下：
其中，FM为管理结构，VM为虚拟机。 ?
可达集
考虑下面一个信条：所有结构管理对于跳跃盒子（内部管理设备）是可达的。
J为“跳跃盒子”
同理我们可以用Datalog语言描述下面这些定义及描述：负载平衡路径的等价性、位置、动态数据包头等。
? 网络优化数据日志（NoD）
?
压缩数据结构
在Datalog中编码一个关系的主要抽象数据结构是一个表格。例如：一个表格是用来储存路由器输入数据包集，一个表格用来储存输出数据包集。为了升级在路由器上输入输出的关系，
（Z3中数据日志结构）通过把这些关系转化成代数关系的方式来运行数据日志。
下面Figure3 表示了一个单独的路由，用ACL（访问控制列表）来drop HTTP数据包，drop80端口数据包。
?
结合Select和Project
仍然使用上面Figure3所展示的例子：最初join的输出是所有有着以1为开始的源地址的可能的输入数据包集产生的，尽管这样看来是很没有效率的路径。下一步是Select之后，所有可能的输入数据包集是1，同时所有的输出数据包的源比特等于1，终点端口不是80端口。最后，最后一步中，生成我们需要的输出数据包。
4. 测试评价：和现存的网络故障诊断工具比较：
上表是大规模测试结果的一个小样本。它展示了在Stanford基准的子集下运行多种测试工具的时间（秒），包括可达性和不可达性的查询，回路检测查询。测试定义了一个5分钟的超时限制和8G的存储限制。
几点说明：注意到，Model checker只能编码可满足性的回答（例如：“一个节点是否是可达