Я реализовал алгоритм консенсуса (на основе Paxos). Я добавил несколько случайных тестовых примеров, и все в порядке. Но хотите провести тестирование с помощью проверки модели? Не удалось найти подходящую статью. Поделитесь, пожалуйста, как сделать с проверкой модели в Paxos
Спасибо
Вы можете использовать средство проверки модели вращения, чтобы проверить абстрактное описание системы.
Для реализаций на основе Java вы можете использовать Java Path Finder.
Также существует mace, где вы можете реализовать и протестировать распределенные системы, такие как Paxos, и он имеет некоторую поддержку для включения C код.
С уважением, Кристиан
