Designing and implementing distributed systems correctly can be quite challenging. Although these systems are often accompanied by formal specifications that are verified using model-checking techniques, a gap still exists between the implementation and its formal specification: there is no guarantee that the implementation is free of bugs. To bridge this gap, we can use model-based testing. Specifically, if the model of the system can be interpreted as a finite-state automaton, we can generate an exhaustive test suite for the implementation that covers all possible states and transitions. In this paper, we discuss how to efficiently generate such a test suite for distributed systems written in the actor model. Importantly, our approach does not require any modifications to the code or interfering with the distributed system execution environment. As an example, we verified an implementation of a replication algorithm based on Viewstamped Replication, which is used in a real-world system.

翻译：正确设计与实现分布式系统具有相当高的挑战性。尽管这些系统通常配有通过模型检验技术验证的形式化规约，但在实现与其形式化规约之间仍存在差距：无法保证实现完全无缺陷。为弥合此差距，可采用基于模型的测试方法。具体而言，若系统模型可解释为有限状态自动机，则可为实现生成覆盖所有可能状态与转换的穷举测试套件。本文探讨如何为基于Actor模型编写的分布式系统高效生成此类测试套件。值得注意的是，我们的方法无需修改代码或干扰分布式系统执行环境。作为示例，我们验证了基于Viewstamped Replication的复制算法实现，该算法应用于实际系统中。