Технология 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.
• Pinery — предназначен для генерации тестовых данных сложной структуры на основе описаний в виде грамматик (к таким описаниям относятся, например, BNF, регулярные выражения, DTD и т. п.).
• 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