Технология UniTESK
UniTESK — технология тестирования на основе формальных спецификаций.
Основные идеи технологии UniTESK следующие:
- Функциональные требования к поведению тестируемой системы представляются в виде контрактных спецификаций. Контракт состоит из предусловий, постусловий на операции, и инвариантов, определяющих ограничения целостности его внутренних данных.
- Критерии тестового покрытия определяются на основе структуры постусловий операций, т.е. в отличие от классических технологий, существует возможность дополнительно к покрытию кода определить покрытие требований. Например, покрытие ветвей в коде постусловия и покрытие дизъюнктов из дизъюнктивной нормальной формы условий этих же ветвлений.
- Тестовый сценарий создается для достижения определённого покрытия заданной группы операций. Основа сценария - конечный автомат, моделирующий поведение тестируемого компонента. Автомат задается таким образом, что покрытие всех его переходов гарантирует покрытие 100% ситуаций в соответствии с выбранным критерием.
- Последовательности тестовых воздействий генерируются при выполнении тестового сценария, во время которого автоматически строится некоторый путь, покрывающий все переходы описываемого им автомата.
Технология сочетается со всеми этапами жизненного цикла разработки программного обеспечения от сбора и анализа требований до сопровождения, не требует для внедрения коренной перестройки процессов.
История создания
- В 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]