- **Основная статья:** Lingzhi Ouyang и соавт. — [Multi-Grained Specifications for Distributed System Model Checking and Verification](https://tianyin.github.io/pub/mspec.pdf). EuroSys 2025, DOI `10.1145/3689031.3696069`.
- **Кратко о статье:** Авторы проверяют ZooKeeper с помощью TLA+ и рассматривают конфликт между точностью модели и размером пространства состояний. Remix позволяет сочетать детальные спецификации целевых модулей с более грубыми спецификациями остальной системы и проверять соответствие модели коду. Подход помог обнаружить шесть серьёзных ошибок. В проекте сравниваются разные гранулярности спецификаций на сокращённых сценариях ZooKeeper.
- **Почему результат актуален:** работа 2025 года проверяет развивающуюся производственную систему; исправления шести найденных ошибок были приняты в ZooKeeper. Локальный демонстрационный путь использует Java 11, Python 3 и Maven и не требует кластера или специализированного оборудования.
- **Артефакты и данные:** [Lingzhi-Ouyang/Remix](https://github.com/Lingzhi-Ouyang/Remix) под Apache-2.0, с ZooKeeper 3.9.1, TLC, генерацией модельных трасс, проверкой соответствия и детерминированным воспроизведением; комитет EuroSys присвоил артефакту знаки Available и Functional. Зафиксированные ревизии: `Lingzhi-Ouyang/Remix@81869f1accc1` (Apache-2.0).
- **Что уже предоставляет артефакт:** Готовы ZooKeeper, смешанная спецификация `generator/MSPEC_2.tla`, генерация и преобразование трасс, их проигрывание и отчёт `matchReport`. Скрипты и демонстрационные трассы разрешено использовать как основу; они не заменяют новый сценарий и независимую проверку команды. Проверенные исходные материалы: [демонстрационные трассы](https://github.com/Lingzhi-Ouyang/Remix/tree/81869f1accc1/traces/demo), [конфигурация TLC](https://github.com/Lingzhi-Ouyang/Remix/blob/81869f1accc1/generator/Zab-simulate.ini).
- **Проверяемый вопрос или утверждение:** смешанная гранулярность спецификации уменьшает стоимость model checking относительно полностью детальной модели и обнаруживает расхождения, которые теряются в полностью грубой модели.
- **Технический результат:** Подготовить грубую, детальную и смешанную спецификации и общий воспроизводимый конвейер: генерация трасс в TLC, преобразование в формат проигрывателя, запуск на малой конфигурации ZooKeeper и автоматический отчёт о совпадениях и расхождениях. Готовый конвейер можно повторно использовать; все варианты должны включать новый сценарий и одинаковые ограничения поиска.
- **Обязательное приращение команды:** Добавить сценарий ZooKeeper, отсутствующий в демонстрационных трассах закреплённой версии, и включить его в сравнение гранулярностей. Для хотя бы одного совпадения или расхождения самостоятельно сопоставить события модели с журналами и состоянием реализации; итогового `matchReport` без этого разбора недостаточно.
- **Эксперимент:** Сравнить три гранулярности по числу состояний, времени проверки и расхождениям на 2–3 сценариях, включая отсутствующий в демонстрации. Хотя бы одно совпадение или расхождение независимо подтвердить по событиям и состоянию ZooKeeper, объяснив их соответствие модели; обнаружение неизвестной ошибки не требуется.
- **Границы выводов:** сравнение относится к выбранным сценариям ZooKeeper и ограничениям поиска TLC; оно не доказывает полноту спецификаций и не оценивает все возможные ошибки реализации.
- **Ресурсный профиль:** Локально, Linux, CPU, 8–16 ГБ памяти. При дорогой генерации уменьшить число событий и конфигурацию ZooKeeper, сохранив три гранулярности, новый сценарий и независимую проверку соответствия. Демонстрационные трассы подходят для проверки конвейера.
Детализировать один дополнительный модуль или изменение ZooKeeper, внести контролируемое расхождение между моделью и кодом либо исследовать границу, после которой дополнительная детализация перестаёт окупаться.
| Дата | Версия | Основание | Изменение обязательного результата |
|---|---|---|---|
| 07.09.2026 | 1.1 | Статический просмотр закреплённого артефакта: готовые сценарии частично покрывают задание. | Добавлены новый сценарий и независимая проверка соответствия реализации; сокращённый путь сохраняет их. |
