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