Тестирование на основе моделей к.ф.-м.н. В. В. Кулямин ИСП РАН. - презентация

1 Тестирование на основе моделей к.ф.-м.н. В. В. Кулямин ИСП РАН

2 Тестирование вообще Тестирование (IEEE 610, SWEBOK): Оценка соответствия системы требованиям к ней на основе результатов наблюдения за ее работой в специально подготовленных ситуациях Система в ходе тестирования должна работать Нужно готовить специальные ситуации – тесты Оценивается соответствие – ищем ошибки Нужна общая оценка – ищем все ошибки

3 «Обычное» тестирование 1. Придумываем ситуацию 2. Оформляем ее в виде сценария взаимодействия теста с системой 3. Понимаем, как должна система вести себя в его рамках 4. Дополняем сценарий проверкой правильности Результат – тестовый вариант (test case) 5. Оцениваем достаточность имеющегося набора ситуаций: достаточно – конец, нет – goto 1

4 «Обычное» тестирование Ограниченная очередь размера 3 1.В начале – пуста 2.put(X) 3.Y = take() 4.assert (Y == X) ? 1.В начале – полна 2.put(X) 3.assert (exception)

5 Зачем здесь модели? Распознавание ошибки – ментальная модель правильной работы Math.abs( ) = Полнота набора ситуаций – ментальная модель всех важных ситуаций При тестировании на основе моделей модели выделяются явно и заранее

6 Используемые модели Конечные автоматы (Finite State Machines, FSM) Программные контракты (Software Contracts)...

7 Конечный автомат (банкомат) Начало Выбор операции Авторизация Карта / Вывести приглашение ввести PIN Корректный PIN / Вывести меню Авторизация 1 Некорректный PIN / Сообщение Авторизация 2 Некорректный PIN / Сообщение Некорректный PIN / Заблокировать карту Сообщение о блокировке Сообщение о выдаче баланса Сообщение о выдаче денег Запрос баланса / Выдать чек Запрос денег / Вывести вопрос о сумме Выбор суммы Сумма / Выдать деньги Время / Вывести исходное сообщение

8 Тестирование на основе FSM Можно ли проверить, ведет ли себя неизвестная реализация всегда так же, как модель? При каких условиях это можно сделать? 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y Модель 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y Реализация

9 Проверка соответствия Требования к модели Полная определенность Минимальность Сильная связность Гипотезы о реализации Реализация – конечный автомат с теми же стимулами и реакциями Полная определенность В начале находимся в начальном состоянии Число состояний ограничено 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y 0 a, b x, y b/yb/y a/xa/x a/ya/y 01 b/yb/y a/xa/x a/xa/x b/yb/y 0 a/xa/x b/yb/y =

10 Методы проверки – обход Построение обхода (transition tour) aababb s = status – возвращает идентификатор состояния sasasbsasbsbssasasbsasbsbs 0x1x1x2y2y0y2 (xxxyyy) 0x1x1x2y2y1x2 (xxxyyx) 0x1x1x2y2y2y2 (xxxyyy) 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y

11 Методы проверки – W-метод 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y reset 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y r = reset – переводит в начальное состояние S – множество последовательностей, достигающих всех состояний S = {ε, a, b} W – множество последовательностей, различающих все состояния W = {a, b} – 0:{x, y}; 1:{x, x}; 2:{y, y} S{a,b}W – полный тест {ε, a, b}{a, b}{a, b} = {aa, ab, ba, bb, aaa, aab, aba, abb, baa, bab, bba, bbb} aarabrbarbbraaaraabrabarabbrbaarbabrbbarbbb xx.xx.yy.yy.xxx.xxx.xxy.xxy.yyy.yyy.yyx.yyy xx.xx.yy.yy.xxx.xxx.xxy.xxy.yyy.yyy.yyy.yyy S{a,b} m-n W – полный тест для больших реализаций

12 Другие методы проверки D-метод различающая последовательность u = ba – 0:yy; 1:xy; 2:yx S{a,b}u abarbbaraabarabbarbabarbbba Методы, работающие без reset Адаптивные методы 0 12 a/xa/x a/xa/x b/xb/x b/yb/y b/yb/y a/ya/y

13 Получаемые тесты abarbbaraabarabbarbabarbbba xxy.yyx.xxxy.xxyx.yyyx.yyyy z = a(); assert(z == x); z = b(); assert(z == x); z = a(); assert(z == y); reset(); … Тесты теперь можно генерировать полностью автоматически, если выполнены все ограничения на модель

14 Конечные автоматы – еще не все Не всякую задачу удобно описывать конечным автоматом Часто можно только очень большим Сложность построения тестов O(p (m-n+1) n 3 ) Чаще всего ограничения на число состояний в реализации неизвестны Часто требования недетерминированы Часто результат в некотором состоянии определен не для всех стимулов

15 Конечные автоматы – еще не все Ограниченная очередь размера 3 [X] [Y] [X, X] [X, Y] [Y, X] [Y, Y] [X, X, X] [X, X, Y] [X, Y, X] [X, Y, Y] [Y, X, X] [Y, X, Y] [Y, Y, X] [Y, Y, Y]

16 Конечные автоматы – еще не все Система управления памятью void* malloc(int n) void free(void* m) malloc(3); malloc(5);malloc(4);malloc(7);

17 Конечные автоматы – еще не все Таймер включитьсигнал выключить Барьер Высота 3 init(3) wait()

18 Программные контракты Система – набор взаимодействующих компонентов Компоненты взаимодействуют с помощью вызовов интерфейсных операций друг друга Каждая операция имеет Предусловие Определяет, когда операцию можно вызывать Постусловие Описывает результаты работы операции

19 Пример контракта Вычисление целочисленного логарифма int logn(int x, int b) pre(b > 1) & (x > 0) postb logn x & b logn+1 > x

20 Что это дает для тестирования? Можно тестировать отдельные компоненты большие подсистемы систему в целом Постусловие дает критерий правильности Тест можно разбить на два компонента Генератор тестовых данных Оракул – проверяет правильность работы на любых данных Можно записывать сложные и недетерминированные ограничения

21 Более сложный пример АРМ компоновщика заказов Показывает список заказов для обработки Позволяет Добавить новый заказ в конец списка Добавить срочный заказ в конец подсписка срочных заказов Пометить заказ как срочный Убрать первый заказ из списка (когда он обработан)

22 Контракт добавления заказов List urgent; List ordinary; int MAX; boolean addOrdinary(Order o) { pre { return true; } post { < MAX) return ordinary ordinary.add(o) ) && urgent && addOrdinary == true ; else return ordinary && urgent && addOrdinary == false ; }

23 Контракт переноса заказа в срочные boolean moveToUrgent(Order o) { pre { return true; } post { o in ordinary )) return ordinary ordinary.remove(o) ) && urgent urgent.add(o) ) && moveToUrgent == true ; else return ordinary && urgent && moveToUrgent == false ; }

24 Контракт удаления заказа Order removeFirst() { pre { return urgent.size != 0 || ordinary.size != 0 ; } post { if(urgent.size != 0) return ordinary && urgent urgent.removeFirst() ) && removeFirst urgent[0] ) ; else return ordinary ordinary.removeFirst() ) && urgent && removeFirst ordinary[0] ) ; }

25 Что получилось? Тестируемая системаМодель true / false Оракул

26 Что еще надо? Проверка правильности Построение тестовых данных Оценка полноты набора тестов + ? ?

27 Полнота тестов Покрытие кода тестируемых функций Метод функциональных диаграмм

28 Покрытие постусловия post { if ( a 3 & !b.closed() ) … else … } a > 0 && !c.isActive() && a 0 && !c.isActive() && b.closed()

29 Покрытия контракта и кода ПостусловиеКод Если покрытие постусловия выше, то покрытие кода выше 100% постусловия и 100% кода не следуют друг из друга

30 Метод функциональных диаграмм +: int × int int int = {positive, 0, negative} Первый аргументВторой аргументПример pos 2, 3 pos02, 0 posneg2, -1 0pos0, 3 000, 0 0neg0, -1 negpos-2, 3 neg0-2, 0 neg -2, -1

31 Метод функциональных диаграмм a > 0 F(b) < 5 isActive(c) f == g(a)-F(b)*b a + 1 f == -1 a f == 0 if(a > 0 && F(b) < 5) return f == g(a)-F(b)*b && a + 1; else if(isActive(c)) return f == -1 && a else return f == 0 && a

32 Пример – ветви постусловий addOrdinary() ordinary.size + urgent.size < MAX ordinary.size + urgent.size == MAX addUrgent() ordinary.size + urgent.size < MAX ordinary.size + urgent.size == MAX moveToUrgent(o) ( o in ordinary ) !( o in ordinary ) removeFirst () urgent.size != 0 ordinary.size != 0 adOrN adOrE adUrN adUrE mvN mvE rmUr rmOr

33 Обобщение состояний, шаг 1 УсловияСостояниеadOradUrmvrm (0, 0)ABDA- (0, 0 < o < M)BB, CE, FEA, B (0, M)CCCFB (0 < u < M, 0)DE, FD, GDA, D (u, o) u+o < MEE, F EB, E (u, o) u+o = MFFFFB, E (M,0)GGGGE

34 Обобщение состояний, шаг 2 addOrN addUrN addOrE, addUrE mvN rmUr mvE rmOr ordinary.size urgent.size 0 0 MAX

35 Редукция сложных автоматов

36 Итоги Программные контракты Оракул Ветви постусловий – важные ситуации Построить обход переходов обобщенного автомата Подготовить тестовые данные (?)

37 В чем цель тестирования? (Дейкстра) Тестирование не может подтвердить правильность, но может найти ошибки => (?) Цель тестирования – поиск ошибок

38 В чем цель тестирования? А как бы мы иначе узнали, что ошибок в программе нет? Тестирование – это метод оценки качества системы Если ошибки есть, оно их должно находить Если их нет, оно должно это подтверждать Оно должно давать еще много информации Какие части системы наиболее устойчивы Где, вероятно, еще есть ошибки и какого рода Достаточно ли высоко качество системы в целом и стоит ли тратить усилия на доработку Модели – способ сделать эту оценку более надежной и объективной