Методы верификации
Верификация встроенных возможностей языка основывается на методе OTK (см. предыдущий подраздел). Целевые конструкции моделируются на формальном языке TreeDL, из формальной модели генерируются тестовые программы. Оракул строится на основе сравнения трассы исполнения тестовой программы, откомпилированной тестируемым компилятором, с трассой выполнения программы, откомпилированной на эталонном компиляторе.
Далее мы будем рассматривать только вопросы тестирования библиотек, предоставляющих поддержку времени исполнения.
Верификация библиотек времени исполнения основывается на методе функционального тестирования с использованием технологии автоматизированного тестирования UniTESK.[].
Рассмотрим основные особенности UniTesK в приложении к тестированию программных интерфейсов:
- разделение построения тестовых воздействий и проверки правильности поведения целевой системы: тестовые воздействия строятся в тестовых сценариях, а проверка правильности поведения целевой системы осуществляется в тестовых оракулах;
- автоматизированное построение тестовых воздействий;
- представление функциональных требований к целевой системе в виде формальных спецификаций;
- автоматическая генерация тестовых оракулов из спецификаций;
- язык описания формальных спецификаций и тестовых воздействий «близок» к языку, на котором разработана целевая система;
- автоматически генерируются критерии качества покрытия требований;
- автоматически производится оценка качества покрытия требований при прогоне тестов.
Метод тестирования с использованием UniTESK подробно рассмотрен в препринте [].
Для работы с формальными спецификациями и спецификациями тестов разработаны пакеты инструментов CTesK [] и JavaTESK [].
Представленный метод использовался при тестировании системы поддержки исполнения компилятора Sun Java 1.4.