Connecting concrete and abstract programs - ligurio/sqa-wiki GitHub Wiki

Validating Traces of Distributed Programs Against TLA+ Specifications⋆ - Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz
Verifying Software Traces Against a Formal Specification with TLA+ and TLC -- Ron Pressler
Validating Traces of Distributed Systems Against TLA+ Specifications -- Stephan Merz
Никита Синяченко, Евгений Чернацкий — TLA+ для эффективного тестирования распределенных систем, Video, Source code
Model Checking Cache Coherence in System-Level Code - Nicholas Allen and Yang Zhao, Oracle Labs Brisbane, June 2016 PDF
Modelator is a tool that enables automatic generation of tests from models. Modelator takes TLA+ models as its input and generates tests that can be executed against an implementation of the model.
Kayfabe: Model-based program testing with TLC - Star Dorminey, Video, PDF
Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы -- П. Н. Девянин, В. В. Кулямин, А. К. Петренко, А. В. Хорошиловe, И. В. Щепетков
Model Checking Guided Testing for Distributed Systems