Тестирование на основе моделей: теория, инструменты, применения Группа спецификации, верификации и тестирования ИСП РАН 2004

Формирование группы Совместный проект ИСП и Nortel Networks Разработка набора функциональных тестов для ядра операционной системы цифровой АТС 1994 – 1996

Результаты первого проекта Разработана технология KVEST автоматизированного построения тестов на основе формальных спецификаций Язык спецификаций – RSL, язык реализации – Protel Разработаны инструменты, поддерживащие KVEST Разработаны формальные спецификации ядра ОС ~60 тыс. строк Разработаны дополнительные компоненты тестов ~100 тыс. строк Сравнение: Код целевой системы ~250 тыс. строк Сгенерированный тестовый набор ~850 тыс. строк Найдено 230 ошибок Из них около 20 приводит к «холодной перезагрузке» ОС

Проблемы тестирования Тестирование призвано измерять качество целевого ПО Как быть с качеством тестов? Проверка соответствия требованиям «Достаточная» представительность Ошибки и «возможные» ошибки Покрытие элементов кода Покрытие требований Нужна модель требований

KVEST: решения Контрактные спецификации: Предусловия и постусловия операций Инварианты типов данных Критерий качества тестирования – покрытие спецификаций Построение конечного автомата по спецификации и заданному уровню покрытия Построение теста во время выполнения – обход конечного автомата Повышение уровня абстракции при разработке тестов

Контрактные спецификации Предусловие описывает область определения операции sqrt(x) pre x 0 Постусловие описывает ограничения на правильные результаты операции sqrt(x) post result*result = x Инвариант типа описывает условия целостности его данных Triangle x,y,z : x+yz & x+zy & y+zx

Целевая система Тестовые оракулы Тестовый оракул Формальные спецификации Тестовые воздействия ?

Виды спецификаций Контрактные Исполнимые Аксиоматические Сценарные Близки к требованиям Абстрактны или конкретны по выбору Удобны для построения оракулов Плохи для построения тестовых последовательностей Часто далеки от требований Обычно слишком конкретны Не вполне удобны для построения оракулов Удобны для построения тестовых последовательностей Далеки от требований Обычно слишком абстрактны Не вполне удобны для построения оракулов Неудобны для построения тестовых последовательностей Близки к требованиям Абстрактны или конкретны по выбору Не вполне удобны для построения оракулов Неудобны для построения тестовых последовательностей

Критерии покрытия Качество тестирования измеряется степенью покрытия тестируемой системы Покрытие спецификаций близко к покрытию требований /* Контроллер лифта */ if Inner_up Outer_up then // двигаться вверх else if Inner_down Outer_down then // двигаться вниз else // стоять на месте

Построение конечного автомата состояния параметрыобласть определения операции цели покрытия

Выполнение теста I Вычисление одного тестового воздействия текущее состояние параметры состояния Был разработан инструмент, автоматически вычисляющий параметры в случае линейных условий

Выполнение теста II 123 Построение тестовой последовательности

Повышение уровня абстракции Целевая система Спецификации – модель поведения Модель теста Критерий покрытия Медиатор

Факторизация автомата

Неявное представление автомата

KVEST: архитектура теста Целевая система Спецификации на RSL Медиаторы на ЯР Скрипт-драйвер на RSL Оракулы на RSL Шаблон скрипт- драйвера Скрипт-драйвер на ЯР Оракулы на ЯР Вставки в шаблон

Другие проекты до 2000 года I Тестирование разных версий ядра ОС АТС Спецификация и тестирование системы настройки телекоммуникационных сервисов базового уровня Перепроектирование подсистемы управления очередями сообщений в ОС АТС Разработка методики автоматизированной генерации документации на естественном языке из спецификаций 1996 –

Другие проекты до 2000 года II Разработка технологии KVEST2 Спецификация и тестирование системы управления очередями сообщений в контроллере смарт-карт Спецификация и тестирование системы управления шлюзом IP-телефонии Разработка технологии ко- верификационной разработки ПО Спецификация и тестирование системы поддержки распеределенных сервисов – – 2000

Недостатки KVEST Несколько языков Трудности построения связи между спецификациями и реализацией Недостаточная структурированность теста Трудности обучения и внедрения

UniTesK Один язык Спецификации и другие компоненты тестов разрабатываются на расширении целевого языка Лучшая структуризация тестов Интеграция с привычными средами разработки

UniTesK: архитектура теста Целевая система Спецификации Медиаторы Медиаторы на ЯР Обходчик Итератор тестовых воздействий Оракулы на ЯР Сценарий

Целевая система UniTesK: разработка тестов Разработка спецификаций Критерии качества Требования Выделение интерфейса Разработка сценариев Разработка медиаторов Выполнение тестов Спецификации Тестовые сценарии Медиаторы Тестовые отчеты Проетные документы Анализ результатов

Параллелизм: модели поведения Асинхронность и распределенность Модели – асинхронные автоматы ?a !x !y !z ?b B : X* P ( R* ) a i { x i } B : X* P ( R* ) a i { y j x k …x l y n : k+…+l = i } ?a !x!y ?e?a !x!y

Распределенность ?a ?{a,b} ?b ?{a,a} ?{b,b} ?{a,a,a} ?{a,a,b} Как моделировать реакции на все возможные комбинации входов? Аксиома простого параллелизма : Реакция на несколько одновременных входов совпадает с реакцией на некоторую их последовательность

Целевая система Генерация тестовых входов s 11 s 21 s 31 s 12 s 32 s 13 s 22 s 23 s 14 s 24 s 33 Вместо тестовой последовательности используется набор последовательностей

Целевая система Сбор реакций Реакции образуют частично упорядоченное множество r 33 r 32 r 12 r 23 r 22 r 11 r 21 r 31 время

Проверка корректности поведения стимулыреакции Аксиома простого параллелизма

Текущее состяние Стационарное тестирование Выполняем (мульти)последовательность и ждем, пока система не «успокоится» Покрытие стимулов и производные Гарантировать покрытие нестационарных состояний нельзя – требуются новые гипотезы

Тестирование компиляторов Спецификации языка Набор базовых блоков модели Тестовые программы Итератор комбинаций Привязка базовых блоков if(…)…else … for(…;…;…)

Проверка корректности оптимизации Тестовое воздействие Компилятор Оптимизатор Компилятор == ?

Поддержка UniTesK – 2002 Java / NetBeans, Eclipse (план) CTesK2000 – 2001 C / Visual Studio 6.0, gcc Link2002 – 2003 Java / NetBeans – 2003 C# / Visual Studio.NET 7.1 OTK2002 – 2003 Инструмент построения тестов для компиляторов

Применения UniTesK Реализации IPv Microsoft Research Мобильный IPv6 (в Windows CE 4.1) Октет Компиляторы Intel Инструменты поддержки UniTesK Пилотные проекты ГосНИИАС Банковская система ведения данных о клиентах Библиотека классов для разработки приложений уровня предприятия Биллинговая система

Участие в обучении МГУ Курс «Формальные спецификации программ» Спецкурс «Методы автоматизации тестирования» Спецсеминар «Верификация и валидация ПО» МФТИ Курс «Языки формальных спецификаций» Спецсеминар «Верификация и валидация ПО» Тренинги по UniTesK Ланит-Терком, Россия Университет Саарланда, Германия Systematic Software Engineering, Дания Luxoft, Россия

Состав группы

Контакты Сайт группы Сайт проектов UniTesK Электронный адрес

Литература I. Burdonov, A. Kossatchev, A. Petrenko, H. Wong. Overview of the Kernel Verification project. BNR Reports, 1997 И. Б. Бурдонов, А. В. Демаков, А. С. Косачев, А. В. Максимов, А. К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. Труды ИСП, т.1, 1999, стр I. Bourdonov, A. Kossatchev, A. Petrenko, D. Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. Proc. FM99, LNCS 1708, Springer-Verlag, 1999, pp И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин. Использование конечных автоматов для тестирования программ. Программирование, т. 26,. 2, 2000, стр A. K. Petrenko, I. B. Bourdonov, A. S. Kossatchev, V. V. Kuliamin. Experiences in using testing tools and technology in real-life applications. Proc. SETT2001, Pune, India, 2001 A.Petrenko. Specification Based Testing: Towards Practice. Proc. PSI2001, LNCS 2244, 2001 I. Bourdonov, A. Kossatchev, V. Kuliamin, A. Petrenko. UniTesK Test Suite Architecture. Proc. FME 2002, LNCS 2391, pp , Springer-Verlag, 2002 И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Асинхронные автоматы: классификация и тестирование. Труды ИСП РАН, т. 4, 2003, стр V. Kuliamin, A. Petrenko, N. Pakoulin, A. Kossatchev, I. Bourdonov. Integration of Functional and Timed Testing of Real-time and Concurrent Systems. Proc. PSI2003. A. Kossatchev, A. Petrenko, S. Zelenov, S. Zelenova. Using Model-Based Approach for Automated Testing of Optimizing Compilers. Proc. Intl. Workshop on Program Undestanding, Gorno-Altaisk, 2003 В.В.Кулямин, А.К.Петренко, А.С.Косачев, И.Б.Бурдонов. Подход UniTesK к разработке тестов. Программирование, т. 29, 6, 2003, стр

Спасибо за внимание