Всякий раз, тестируя программу, мы явно или неявно строим модель её поведения. Иногда это всего лишь ментальная модель, находящаяся в голове тестировщика. Иногда эта модель описывается текстом, например, в форме вариантов использования. Иногда полезно зафиксировать эту модель в виде какой-нибудь диаграммы или схемы. Но все эти модели не являются формальными, поэтому построить тесты на их основе может только человек. Однако существуют техники и инструменты, позволяющие описать формальную модель поведения так, чтобы из неё можно было автоматически сгенерировать тесты, проверяющие соответствие реального поведения программы этой модели. Именно о таких инструментах и будет идти речь на этом семинаре: UniTESK, SpecExplorer, NModel.