Воркшоп: TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов

Разрабатывать конкурентные системы сложно. Самые плохие ошибки закладываются в алгоритм, не находятся никакими тестами, и ждут своей уникальной последовательности событий, чтобы взорваться и всё испортить. Но находить такие ошибки можно, даже не написав ни строчки кода на Go -- если воспользоваться методами формальной верификации. Один из таких методов — разработанный Лесли Лампортом формализм TLA+ и инструмент верификации TLC -- идеально подходит верификации конкурентных систем на Go. Мы поговорим про TLA+/TLC, про PlusCal — транслируемый в TLA+ язык спецификации алгоритмов специально для инженеров, а также про практики применения TLA+/TLC в проектах на Go. В ходе воркшопа мы напишем и разберем несколько простых низкоуровневых моделей алгоритмов работы с каналами в Go, а также попробуем разобрать относительно высокоуровневую модель сервиса. Вводная часть:    • TLA+/TLC: практичный инструмент форма...   Воркшоп будет проходить в среде MS Visual Studio Code (
/). Вам понадобится плагин TLA+ (
, и, возможно, плагин для Golang (
Исходники слайдов, а также исходные тексты этого воркшопа:
Трансляция кода: