Инструменты генерации тестовых данных для функционального тестирования микропроцессоров и интерфейсов программных систем д.ф.-м.н., проф.каф.СП Александр Константинович Петренко асп. Евгений Корныхин

Генерация тестовых программ на основе грамматик (БНФ) BNFTool: возможности: простой способ генерации программ в некотором синтаксисе ограниченность: только синтаксически правильные программы и нет возможности нацелить на отдельные конструкции языка

Генерация на основе моделей программ OTK, Pinery: графовые модели для задания свойств программ возможности: позволяет нацеливать тест ограниченность:не учитывает состояние исполняемой программы (например, значения переменных)

Генерация на основе «шаблонов» программ Pex, Genesys-Pro, RAVEN «шаблон» - скелет тестирующей программы возможность нацеливания на свойства исполнения программ ограниченность: несложные структуры состояния (для Pex это серьезное ограничение, для Genesys-Pro – норма)

Генерация на основе «шаблонов» программ программа на языке ассемблера шаблон программы эксперт ~ 100 шаблонов, длина шаблонов = мало (преамбула для r2,r3) AND r1, r2, r3 LOAD r4, r2, 66 AND r1, r2, normal LOAD r4, r2, l1Hit

... LOAD x, y, tlbHit STORE z, tlbMiss... Общая схема генерации (= 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 модель инструкции constraint v = 145 y = 52 с = значения параметров шаблона... LOAD x, y, 66 STORE z, x, программа на языке ассемблера

Практическая важность результата длина/сложность шаблона увеличивается с 2-3 до обозримое число шаблонов (то есть и целей тестирования) увеличивается на два порядка (~100 ~10000)

Исходные данные и модели (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 с = значения параметров шаблона... LOAD x, y, программа на языке ассемблера

Практическая важность результата длина/сложность шаблона увеличивается с 2-3 до обозримое число шаблонов (то есть и целей тестирования) увеличивается на два порядка (~100 ~10000)

Pex

Pex (2)

Genesys-Pro (2)