Краткий обзор технологии тестирования UniTESK
Технология тестирования UniTESK [-] была разработана в Институте системного программирования РАН [] на основе опыта, полученного при разработке и применении технологии KVEST (kernel verification and specification technology) []. Общими чертами этих технологий являются использование формальных спецификаций в форме пред- и постусловий интерфейсных операций и инвариантов типов данных для автоматической генерации оракулов (компонентов тестовой системы, осуществляющих проверку правильности поведения целевой системы), а также применение конечно-автоматных моделей для построения последовательностей тестовых воздействий (тестовых последовательностей). В отличие от технологии KVEST, в которой для спецификации требований использовался язык RSL (RAISE specification language) [], технология UniTESK использует расширения широко известных языков программирования.
