Проверка модели Paxos

Question

Я реализовал согласованный алгоритм (на основе Paxos). Я добавил несколько случайных тестовых случаев, и, кажется, все в порядке. Но хотите провести тестирование с помощью проверки модели? Не могу найти правильную статью для этого. Пожалуйста, поделитесь, как поступить с проверкой модели в Паксосе.

Спасибо

Answer 1

Вы можете использовать проверку Spin Model, чтобы проверить абстрактное описание системы.

Для реализаций на основе Java вы можете использовать Java Path Finder.

Существует также mace, где вы можете реализовывать и тестировать распределенные системы, такие как Paxos, и он имеет некоторую поддержку для включения C-кода.

С уважением, Кристиан