Interested Article - Технология 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 ( ) (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 (недоступная ссылка)