UniTESK

UniTESK (Unified Testing & specification toolKit) — технология тестирования программного и аппаратного обеспечения на основе формальных спецификаций, разработанная в Институте системного программирования РАН. Технология представляет собой сочетание хорошо зарекомендовавших себя техник, которые могут применяться в различных комбинациях, взаимно сочетаясь и усиливая друг друга. Это делает технологию гибкой и настраиваемой под существующие процессы разработки на всех этапах жизненного цикла разработки программного обеспечения от сбора и анализа требований до сопровождения.

Основу для вынесения вердиктов о правильности поведения тестируемой системы составляют контрактные спецификации в форме пред- и постусловий, написанные на расширениях традиционных языков программирования, таких как C, критерии покрытия обеспечивают прослеживаемость требований.

Успешно использующиеся на практике, техники построения тестов на основе обхода графов состояний позволяют существенно минимизировать количество создаваемого вручную программного кода, вместе с тем обеспечивая разнообразие и массивность тестового набора.

Техники абстракции данных и критерии покрытия, основанные на требованиях, позволяют гибко управлять размером тестового набора и направлять генерацию на покрытие определенных требований, минимизируя тем самым время выполнения тестового набора.

Специальный промежуточный слой, имеющийся в технологии, позволяет быстро настраивать тестовый набор на различные реализации с той же функциональностью.

Все эти техники обеспечивают высокое качество тестирования, прослеживаемость требований и высокий уровень переиспользования компонентов тестового набора при минимуме ручной работы и приемлемом времени выполнения тестов.

Шаги технологии

Определение тестируемой части системы 

На этом шаге определяется тестируемая функциональность, т.е. часть возможностей рассматриваемой системы, которую надо проверить, и тестируемый интерфейс, т.е. способ доступа к проверяемым возможностям.

Определение и анализ требований к тестируемой системе 

На основе анализ всех входных данных, коммуникации с заказчиком, экспертами и пользователями выделяются и систематизируются требования к тестируемой системе. Которые далее представляются в виде формальной модели.

Определение и анализ требований к полноте тестирования 

Выделяются критерии полноты тестирования, которые отражаются на формальной модели.

Разработка тестов 

Разработка источников тестовых данных и модели тестирования в целом.
Основные техники.
Перебор конечных множеств, перебор комбинаций, перебор граничных значений и близких к ним, перебор узловых и близких значений, перебор грамматических конструкций с помощью модульных генераторов, перебор с фильтрацией, перебор атрибутированных графов и последовательностей.
Конечные автоматы, системы помеченных переходов, неявное представление автоматных моделей, послойное тестирование сложных моделей.

Разработка адаптеров, привязывающих тесты к тестируемой реализации 

Отладка и выполнение тестов

Анализ результатов тестирования

История создания

• В 1994 году Институт Системного Программирования Российской Академии Наук (ИСП РАН) по контракту с Nortel Networks разработал методологию и комплект инструментов автоматизации тестирования интерфейсов прикладных программ (API). Первым практическим применением методологии стало ядро операционной системы реального времени.
• В течение 1994—1999 годов ИСП РАН создал и установил в Nortel Networks несколько версий технологии KVEST-1.
• В 1998—1999 годах было завершено создание технологии KVEST-2.
• В 2000 году технология KVEST адаптируется для использования в проектах на языках C и C++.
• В 1999 году ИСП РАН начал разработку технологии верифицирования нового поколения — UniTESK (Unified Testing & specification toolKit).

Применение на практике

Технология была успешно применена во многих проектах. Наиболее интересные:

• Open Linux VERification (OLVER) (c 2005 г.);
• Тестирование интеграционных и биллинговых компонентов Вымпелкома (c 2007 г.);
• Тестирование мобильной реализации протокола
• Тестирование (2000, 1 человеко-год);
• Тестирование компонентов (1999—2000, 6 человеко-лет);
• Тестирование и редизайн системы поддержки приложений (1998—1999, 2 человеко-года);
• Тестирование ядра операционной системы (1994—1997, 25 человеко-лет).

Инструментальная поддержка

• CTESK — инструмент для тестирования программного обеспечения, реализованного на языке C.
• CTESK Community Edition — бесплатная полнофункциональная версия инструмента CTESK для платформы Java.
• Pinery — предназначен для генерации тестовых данных сложной структуры на основе описаний в виде грамматик (к таким описаниям относятся, например, BNF, регулярные выражения,
• OTK (Optimizer Testing Kit) — инструмент для тестирования программных систем, работающих с данными, имеющими сложную структуру. Применение OTK наиболее эффективно при тестировании компиляторов или других систем обработки формального текста. Основной акцент в OTK делается на построении разнообразных входных тестовых данных.
• SynTESK (Syntax Testing Kit) — инструмент для тестирования синтаксических анализаторов (парсеров) формальных языков. SynTESK позволяет проверять соответствие реализации парсера и спецификации данного формального языка, то есть что парсер распознает именно данный формальный язык.

Литература

• Кулямин В. В.. Критерии тестового покрытия, основанные на структуре контрактных спецификаций //Труды ИСП РАН, Подход UniTESK: итоги и перспективы. 14(1):89-107, 2008 [1]
• Гриневич А. И., Кулямин В. В., Марковцев Д. А., Петренко А. К., Рубанов В. В., Хорошилов А. В. Использование формальных методов для обеспечения соблюдения программных стандартов //Труды ИСП РАН, Обеспечение надежности и совместимости Linux-систем. 10:51-68, 2006 [2]
• Бурдонов И. Б., Косачев А. С., Кулямин В. В.. Неизбыточные алгоритмы обхода ориентированных графов: недетерминированный случай //Программирование. 30(1):2-17, 2004 [3]
• Бурдонов И. Б., Косачев А. С., Кулямин В. В.. Использование конечных автоматов для тестирования программ //Программирование. 26(2):61-73, 2000 [4]
• Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A.. UniTesK Test Suite Architecture //Proc. of FME 2002. LNCS 2391, pp. 77-88, Springer-Verlag, 2002. ISBN 3-540-43928-5
• Bourdonov I. B., Demakov A. V., Jarov A. A., Kossatchev A. S., Kuliamin V. V., Petrenko A. K., and Zelenov S. V.. Java Specification Extension for Automated Test Development //Proceedings of PSI'2001. Novosibirsk, Russia, July 2-6, 2001. LNCS 2244:301-307, Springer-Verlag, 2001. ISBN 978-3-540-43075-9 [5]
• Bourdonov I., Kossatchev A., Petrenko A., and Galter D.. KVEST: Automated Generation of Test Suites from Formal Specifications //FM’99: Formal Methods. LNCS 1708, Springer-Verlag, 1999, pp. 608—621. ISBN 3-540-66587-0 [6]

Ссылки

• Основной сайт
• Статья Подход UniTesK к разработке тестов: достижения и перспективы
• Верификация ОС Linux на соответствие стандарту LSB
• Online сервис Pinery: Генерация на основе регулярных выражений Perl