Краткий обзор UniTesK
Данный раздел содержит беглое введение в UniTesK. Более подробное описание можно найти в [2]. С 1994 года в ИСП РАН активно разрабатываются методы и инструменты тестирования программного обеспечения на основе формальных методов.
В 1994-1999 годах по контрактам с Nortel Networks в ИСП РАН был разработан и активно использовался метод тестирования KVEST [7][]. Этот метод отличался от обычных методов тестирования индустриального программного обеспечения тем, что в KVEST использовались формальные спецификации в форме пред- и постусловий для построения тестовых оракулов, а также модель конечных автоматов для построения тестовых воздействий.
Применение KVEST показало, что формальные методы можно с большим успехом применять при тестировании индустриального программного обеспечения. Опыт применения KVEST также показал, что использование академических языков формальных спецификаций и специальных языков описания тестов препятствует встраиванию инструментов, основанных на этих языках, в процесс разработки ПО. Чем ближе язык спецификаций к языку, на котором ведется разработка, тем проще разработчикам писать спецификации и тесты [8].
UniTesK разрабатывался на основе опыта, полученного при разработке и применении KVEST. Рассмотрим основные особенности UniTesK:
- Разделение построения тестовых воздействий и проверки правильности поведения целевой системы. Тестовые воздействия строятся в тестовых сценариях, а проверка правильности поведения целевой системы производится в тестовых оракулах.
- Автоматизированное построение тестовых воздействий
- Представление функциональных требований к целевой системе в виде формальных спецификаций
- Для записи формальных спецификаций используется язык, «близкий» к языку, на котором разработана целевая система
- Автоматическая генерация тестовых оракулов из спецификаций
- Оракулы и реализация связаны посредством тонкой прослойки медиаторов.
- Язык описания тестовых воздействий «близок» к языку, на котором разработана целевая система
- Автоматически генерируются критерии качества покрытия требований
- Автоматически производится оценка качества покрытия требований при прогоне тестов
