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

Question

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

Благодарности

Answer 1

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

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

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

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