Программирование для встроенных систем - статьи

       

Краткий обзор UniTesK


Данный раздел содержит беглое введение в UniTesK. Более подробное описание можно найти в [2]. С 1994 года в ИСП РАН активно разрабатываются методы и инструменты тестирования программного обеспечения на основе формальных методов.

В 1994-1999 годах по контрактам с Nortel Networks в ИСП РАН был разработан и активно использовался метод тестирования KVEST [7][]. Этот метод отличался от обычных методов тестирования индустриального программного обеспечения тем, что в KVEST использовались формальные спецификации в форме пред- и постусловий для построения тестовых оракулов, а также модель конечных автоматов для построения тестовых воздействий.

Применение KVEST показало, что формальные методы можно с большим успехом применять при тестировании индустриального программного обеспечения. Опыт применения KVEST также показал, что использование академических языков формальных спецификаций и специальных языков описания тестов препятствует встраиванию инструментов, основанных на этих языках, в процесс разработки ПО. Чем ближе язык спецификаций к языку, на котором ведется разработка, тем проще разработчикам писать спецификации и тесты [8].

UniTesK разрабатывался на основе опыта, полученного при разработке и применении KVEST. Рассмотрим основные особенности UniTesK:

  • Разделение построения тестовых воздействий и проверки правильности поведения целевой системы. Тестовые воздействия строятся в тестовых сценариях, а проверка правильности поведения целевой системы производится в тестовых оракулах.
  • Автоматизированное построение тестовых воздействий
  • Представление функциональных требований к целевой системе в виде формальных спецификаций
  • Для записи формальных спецификаций используется язык, «близкий» к языку, на котором разработана целевая система
  • Автоматическая генерация тестовых оракулов из спецификаций
  • Оракулы и реализация связаны посредством тонкой прослойки медиаторов.
  • Язык описания тестовых воздействий «близок» к языку, на котором разработана целевая система
  • Автоматически генерируются критерии качества покрытия требований
  • Автоматически производится оценка качества покрытия требований при прогоне тестов



Содержание раздела