TLA+

TLA+ — формальна мова специфікації, розроблена Леслі Лампортом і використовується для проектування, моделювання, документування й перевірки програм, особливо розподілених систем. TLA+ описана як вичерпно перевірений псевдокод, і її використання подібне до креслення; TLA є англійською абревіатурою для часової логіки дій.

TLA+
Парадигма	Action
Дата появи	23 квітня 1999; 26 років тому (1999-04-23)[1]
Творці	Леслі Лампорт
Мова реалізації	Java
Операційна система	багатоплатформенна
Ліцензія	MIT License[2]
Звичайні розширення файлів	.tla
Вебсайт	research.microsoft.com/en-us/um/people/lamport/tla/tla.html

Що стосується дизайну та документації, TLA + виконує ту саму мету, що й неофіційні технічні умови. Однак специфікації TLA+ написані мовою логіки та математики, і точність специфікацій, написаних цією мовою, призначена для виявлення вад дизайну до початку впровадження системи.

Оскільки специфікації TLA + написані офіційною мовою, вони піддаються перевірці з обмеженою моделлю. Модель перевірки знаходить усі можливі поведінки системи до деякої кількості етапів виконання та вивчає їх на порушення бажаних властивостей інваріантності, таких як безпека та життєздатність. Технічні характеристики TLA+ використовують базову теорію множин для визначення безпеки та часову логіку для визначення життєдіяльності.

TLA+ також використовується для написання перевірених машиною доказів правильності як алгоритмів, так і математичних теорем. Докази написані в декларативному, ієрархічному стилі, незалежному від теореми. Як формальні, так і неофіційні структуровані математичні докази можуть бути записані у TLA+; мова схожа на LaTeX, і існують інструменти для перекладу специфікацій TLA+ до документів LaTeX.

TLA+ була введена в 1999 році, після кількох десятиліть досліджень методу верифікації для одночасних систем. З тих пір було розроблено ланцюжок інструментів, що включає IDE та розподілену перевірку моделей. TLA+2 було оголошено у 2014 році, розширивши мовну підтримку для конструкцій із підтвердженням.