Формальная модель требований, используемая в процессе генерации кода приложения и кода тестов

Рассматривается модель, используемая при ручной разработке спецификаций приложения, созданная на основе теории базовых протоколов А.А. Летичевского и поддерживающего теорию инструментария символьной верификации. Обсуждаются способы ограничения поведенческих характеристик модели при условии сохранения соответствия исходным требованиям. По успешно верифицированной модели генерируется код приложения и код тестов. Приводится описание методики применения разработанной модели.