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

Презентация:



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

Исследование и разработка методов генерации тестовых программ для проверки модулей управления памяти микропроцессоров Корныхин Евгений науч.рук-ль: проф.каф.СП,
Автоматическое построение тестов для аппаратного обеспечения с использованием разрешения ограничений проф. А.Петренко, Е.Корныхин.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Корныхин Евгений Валерьевич научный руководитель: д.ф.-м.н. Петренко.
Автоматическое построение тестов для аппаратного обеспечения с использованием разрешения ограничений проф. А.Петренко, Е.Корныхин.
Автоматическое построение тестов для аппаратного обеспечения с использованием разрешения ограничений проф. А.Петренко, Е.Корныхин.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин ИСП РАН / кафедра СП ВМК МГУ научный руководитель:
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин кафедра СП ВМК МГУ научный руководитель: д.ф.-м.н.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин ИСП РАН / кафедра СП ВМК МГУ научный руководитель:
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин кафедра СП научный руководитель: д.ф.-м.н. А. К.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин науч.рук-ль: проф. А.К.Петренко.
Исследование методов генерации программ для тестирования модулей управления памяти микропроцессоров Корныхин Евгений.
Метод генерации тестовых данных для арифметических операций MIPS64.
Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин научный руководитель: д.ф.-м.н. А.К.Петренко.
Транксрипт:

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

План Задача генерации тестовых программ Генерация на основе грамматик (на основе 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)