Автоматическая валидация распределенных алгоритмов

Есть различные категории распределенных алгоритмов. Я буду говорить об алгоритмах, в которых подсистемы стремятся к достижению общего результата, не обладая информацией о том, были ли отправленные ими сообщения обработаны получателями.

Сложность таких алгоритмов превышает когнитивные способности человека, поэтому для их разработки необходимо использовать специальные инструменты. Я расскажу о TLA+ — языке + программном пакете, которые:

1. Дают нотацию для формального описания алгоритма.
2. Моделируют все возможные сценарии исполнения алгоритма, выявляя:
   • не/достижимость недопустимых состояний;
   • достижимость цели алгоритма.

Овладение TLA+ позволит поднять надежность создаваемых вами распределенных алгоритмов на принципиально новую высоту.

Примеры кода будут на языке C#.