EuroSys 2023 Paper 论文阅读笔记整理
问题
分布式系统已成为云计算的支柱，不正确的系统设计和实现可能严重影响分布式系统的可靠性。尽管使用形式化规范建模的分布式系统设计可以通过形式化模型检查进行验证，但要弄清其相应的实现是否符合已验证的规范仍然是具有挑战性的。不正确的系统实现可能违反其已验证的规范，导致复杂的错误。
现有方法局限性
研究人员提出了许多方法来检测分布式系统实现中的错误，可以分类为三类：
-
形式验证框架[41, 42, 67]，以细化的方式验证分布式系统实现的属性。然而，验证过程复杂且耗时。通常需要多人年的工作量来验证系统实现[58]。
-
基于模型的测试[31, 44, 51]，利用抽象模型生成测试用例，以测试分布式系统实现中的特定属性或行为。例如，Modulo [44]对分布式存储系统中的数据一致性属性建模，并生成测试用例以查找收敛故障错误。
-
实现级别的模型检查器[47, 57, 64, 68, 69]，专门设计用于在分布式系统实现中发现错误。在运行时拦截和重排序非确定性的分布式事件（例如，消息和故障）。但它们无法了解目标系统的预期执行结果（即，测试用例的 Oracle），并依赖开发人员手动编写特定系统属性或行为的通用断言来揭示错误。
本文方法
我们提出了一种分布式系统测试技术，即模型检查引导测试（Model checking guided testing，Mocket），以弥合分布式系统中规范和其实现之间的差距。给定目标分布式系统的 TLA+ [45] 规范，我们分析通过验证规范生成的验证状态，并为系统实现生成测试用例。将 TLA+ 规范映射到系统实现中的相应代码之后，进一步确定性地强制系统执行遵循从验证规范生成的测试用例。在系统测试期间，监视系统的运行时状态并将其与 TLA+ 规范中的相应验证状态进行比较。我们使用形式化模型检查生成的状态空间来引导对系统实现的测试，并发现目标分布式系统中的错误。
为了评估Mocket的可行性和有效性，我们将其应用于三个流行的分布式系统，并在它们中发现了3个先前未知的错误。
限制：
-
Mocket需要开发人员手动操作。
-
Mocket要求TLA+规范应该接近相应的实现。
-
在某些场景下，Mocket可能会错过目标系统中的一些实现错误：TLA+规范并没有涵盖分布式系统的所有实现细节；系统实现中的某些并发性没有在TLA+规范中正确建模；省略了一些可能触发目标系统中实现错误的路径。
-
Mocket只能在基于Java的分布式系统上工作。
开源代码：GitHub - tcse-iscas/Mocket: TLA+ model checking guided testing for distributed systems
总结
针对分布式系统的故障检测。作者提出Mocket，需要给定目标分布式系统的TLA+规范，分析规范生成的验证状态，为系统实现生成测试用例。将 TLA+ 规范映射到系统实现中的相应代码之后，进一步确定性地强制系统执行遵循从验证规范生成的测试用例。在系统测试期间，监视系统的运行时状态并将其与 TLA+ 规范中的相应验证状态进行比较。并发现目标分布式系统中的错误。
