Тестирование на основе спецификации реализованных в акторной модели практических распределенных систем
Статья: Тестирование на основе спецификации реализованных в акторной модели практических распределенных систем
Статья в выпуске: 3 т.15, 2026 года.
Бесплатный доступ
Корректная реализация распределенной системы может являться очень сложной задачей. Несмотря на то что распределенные системы часто разрабатываются на основе формальных спецификаций, которые верифицируются при помощи техник проверки моделей, существует значимая разница между формальной спецификацией и реализацией распределенной системы: верификация формальной спецификации не может гарантировать отсутствия ошибок в реализации. Для решения этой проблемы можно использовать тестирование на основе спецификации. Для этого будем интерпретировать формальную спецификацию системы как конечный автомат, и на основе этой спецификации генерировать исчерпывающий набор тестов, покрывающий все возможные состояния и переходы распределенной системы. В этой статье обсуждаются способы эффективной генерации такого набора тестов для распределенной системы, реализованной в акторной модели. Разработанный подход не требует модификации кода реализованной в акторной модели распределенной системы или какого-либо вмешательства в работу среды передачи данных. В качестве примера была верифицирована реализация алгоритма репликации, использующаяся в базах данных компании vk.com, основанная на алгоритме Viewstamped Replication.
Короткий адрес: https://sciup.org/147255445
IDS: 147255445 | УДК: 004.051 | DOI: 10.14529/cmse260303
Model-based Testing of Practical Distributed Systems in Actor Model
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.
