Технология UniTESK

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

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

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

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

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

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

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

История создания 
 В 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 г.);
 Тестирование мобильной реализации протокола IPv6 (2002—2003, 2 человеко-года);
 Тестирование Object Broker (2000, 1 человеко-год);
 Тестирование компонентов ATM Framework (1999—2000, 6 человеко-лет);
 Тестирование и редизайн системы поддержки приложений (1998—1999, 2 человеко-года);
 Тестирование ядра операционной системы (1994—1997, 25 человеко-лет).

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

Литература 
 Кулямин В. В.. Критерии тестового покрытия, основанные на структуре контрактных спецификаций //Труды ИСП РАН, Подход UniTESK: итоги и перспективы. 14(1):89-107, 2008 
 Гриневич А. И., Кулямин В. В., Марковцев Д. А., Петренко А. К., Рубанов В. В., Хорошилов А. В. Использование формальных методов для обеспечения соблюдения программных стандартов //Труды ИСП РАН, Обеспечение надежности и совместимости Linux-систем. 10:51-68, 2006 
 Бурдонов И. Б., Косачев А. С., Кулямин В. В.. Неизбыточные алгоритмы обхода ориентированных графов: недетерминированный случай //Программирование. 30(1):2-17, 2004  
 Бурдонов И. Б., Косачев А. С., Кулямин В. В.. Использование конечных автоматов для тестирования программ //Программирование. 26(2):61-73, 2000 
 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 
 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

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

Тестирование программного обеспечения