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

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

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

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

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

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

6 ... 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, программа на языке ассемблера

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

8

9 Исходные данные и модели (1) Описание шаблона (параметрически заданная тестовая программа)... STORE z, x, tlbMiss LOAD x, y, tlbHit... параметр инструкция

10 Исходные данные и модели (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];

11 Исходные данные и модели (3) Описания моделей компонентов микропроцессора (управление памятью, конвейер и др.) на ЯП AddrTrans (…) {…..} LoadMem (…) {…..}

12 Реализация подхода для тестирования микропроцессоров Шаблон задает класс тестовых ситуаций – цель шаблона Параметры шаблонов – значения аргументов инструкций вычисляются как решение системы ограничений (уравнений), позволяющее достичь цели шаблона Ограничения формулируются на основе описания моделей компонентов Решатель - Z3

13 ... 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, программа на языке ассемблера

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

15 Pex

16 Pex (2)

17 Genesys-Pro (2)