Тестирование на основе моделей: теория, инструменты, применения В. Кулямин, А. Петренко

Тестирование и современное ПО Тестирование призвано измерять качество целевого ПО на основе мониторинга его работы в различных ситуациях Современное ПО отличается повышенной сложностью

Тестирование на основе моделей Исчерпывающее тестирование на практике невозможно Но возможно строить тесты систематически – на основе некоторой «системы» Эта система задается при помощи модели или спецификации

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

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

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

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

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

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

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

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

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

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

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

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

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

Параллелизм: модели поведения Асинхронность и распределенность Модели – асинхронные автоматы ?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 Проведенные тренинги Ланит-Терком, Россия Университет Саарланда, Германия Systematic Software Engineering, Дания Luxoft, Россия Intel, Россия

Контакты Сайт группы Сайт проектов 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, стр

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