Инструменты генерации тестовых данных для функционального тестирования микропроцессоров и интерфейсов программных систем д.ф.-м.н., проф.каф.СП Александр Константинович Петренко асп. Евгений Корныхин
План Задача генерации тестовых программ Генерация на основе грамматик (на основе BNF - BNFTool) (возможности и ограниченность (только синтаксически правильные программы и нет возможности нацелить на отдельные конструкции языка)) Генерация на основе моделей (заготовок) программ (OТК/Pinery) (возможности (позволяет нацеливать тест) и ограниченность (не учитывает сложность внутреннего состояния исполняемой программы)) Два примера зрелых инструментов, использующих для нацеливания шаблоны программ/параметрически заданный тест (Pex, Genesys-Pro) Ограничения – простые структуры данных Для Pex – это серьезное ограничение, для Genesys-Pro – норма (но Genesys-Pro недоступен) Реализация подхода для тестирования микропроцессоров Описания шаблонов (параметрически заданная тестовая программа) Описания моделей инструкций («транслируются» из описания архитектуры в ЯП) Описания моделей компонентов микропроцессора (управление памятью, конвейер и др.) на ЯП Шаблон задает класс тестовых ситуаций – цель шаблона. Параметры шаблонов – значения аргументов инструкций вычисляются как решение системы ограничений (уравнений), позволяющее достичь цели шаблона. Решатель - Z3. Общая схема Практическая важность результата (число шаблонов (то есть и целей тестирования) увеличивается на два порядка, длина/сложность шаблона уведичивается с 2-3 до 10-15)
Генерация тестовых программ на основе грамматик (БНФ) BNFTool: возможности: простой способ генерации программ в некотором синтаксисе ограниченность: только синтаксически правильные программы и нет возможности нацелить на отдельные конструкции языка
Генерация на основе моделей программ OTK, Pinery: графовые модели для задания свойств программ возможности: позволяет нацеливать тест ограниченность:не учитывает сложность внутреннего состояния исполняемой программы
Генерация на основе «шаблонов» программ Pex, Genesys-Pro, RAVEN «шаблон» - скелет тестирующей программы возможность нацеливания на [динамические свойства] программ ограничения: простые структуры данных (для Pex это серьезное ограничение, для Genesys-Pro – норма)
... LOAD x, y, tlbHit... Общая схема генерации (= v (+ y c)) LOAD x, y, c: v y + c; AddrTr(v,p);... (= t (extract[30:10] v)) (or (= t t1) (= t t2)) шаблон программы t структурная модель MMU генерация ограничений tlbHit(t, ts) { «(or » (t1:ts)«(= t t1)» «)» } tlb модель MMU модель инструкции ограничения v = 145 y = 52 с = 66 х = 3... значения параметров шаблона... LOAD x, y, тестовая программа
Исходные данные и модели (1) Описание шаблона (параметрически заданная тестовая программа)... STORE z, x, tlbMiss LOAD x, y, tlbHit... параметр инструкция
Исходные данные и модели (2) Описание моделей инструкций LOADWORD x, y, c: vAddr y + c; vAddr[1:0] = 0; AddrTrans(vAddr, pAddr); pAddr pAddr[35:3] || (pAddr[2:0] + 4); LoadMem(pAddr, memdw); x memdw[vAddr[2:0]:0];
Исходные данные и модели (3) Описания моделей компонентов микропроцессора (управление памятью, конвейер и др.) на ЯП AddrTrans (…) {…..} LoadMem (…) {…..}
Реализация подхода для тестирования микропроцессоров Шаблон задает класс тестовых ситуаций – цель шаблона Параметры шаблонов – значения аргументов инструкций вычисляются как решение системы ограничений (уравнений), позволяющее достичь цели шаблона Ограничения формулируются на основе описания моделей компонентов Решатель - Z3
... LOAD x, y, tlbHit... Общая схема генерации (= v (+ y c)) LOAD x, y, c: v y + c; AddrTr(v,p);... (= t (extract[30:10] v)) (or (= t t1) (= t t2)) шаблон программы t структурная модель MMU генерация ограничений tlbHit(t, ts) { «(or » (t1:ts)«(= t t1)» «)» } tlb модель MMU модель инструкции ограничения v = 145 y = 52 с = 66 х = 3... значения параметров шаблона... LOAD x, y, тестовая программа
Практическая важность результата длина/сложность шаблона увеличивается с 2-3 до обозримое число шаблонов (то есть и целей тестирования) увеличивается на два порядка (~100 ~10000)
Pex
Pex (2)
Genesys-Pro (2)