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

В работе предложен метод автоматизации конструирования генераторов тестовых программ для микропроцессоров. Метод основан на отделении реализации техник генерации тестовых программ от знания об архитектуре тестируемого микропроцессора. Информация, необходимая для генерации тестовых программ, извлекается из формальных спецификаций архитектуры. Полученные результаты могут послужить основой для разработки архитектурно-независимых техник генерации тестовых программ и создания программных инструментов, основанных на анализе формальных спецификаций. Кроме этого, эти результаты могут использоваться в исследовательских проектах и учебных курсах по проектированию и верификации микропроцессоров.

На основе предложенного метода разработан программный инструмент, позволяющий автоматизировать на основе формальных спецификаций конструирование генераторов тестовых программ для микропроцессоров. Разработанный инструмент был применен для создания генераторов тестовых программ для архитектур MIPS64, ARMv8, PowerPC и RISC-V. Генераторы тестовых программ для MIPS64 и ARMv8 используются в отечественных и зарубежных компаниях. Помимо этого, разработанный инструмент может быть использован для создания генераторов тестовых программ для широкого спектра других микропроцессорных архитектур.

Методология и методы исследования

Методологическую основу исследования составляют теория компиляторов, теория формальных языков, теория автоматов, теория множеств, теория графов, теория алгоритмов и математическая логика.

Апробация работы

Основные положения работы обсуждались на следующих конференциях и семинарах:

· Международная конференция «Design Automation Conference», выставка University Booth (г. Остин, США, 2-7 июня 2013 г. и г. Сан-Франциско, США, 2-5 июня 2014 г.);

· Международная конференция «Design, Automation & Test in Europe», выставка University Booth (г. Гренобль, Франция, 18-22 марта 2013 г.; г. Дрезден, Германия, 24-28 марта 2014 г.; г. Гренобль, Франция, 10-12 марта 2015 г.; г. Лозанна, Швейцария, 28-30 марта 2017 г.);

· Международный коллоквиум молодых исследователей в области программной инженерии «Spring/Summer Young Researchers' Colloquium on Software Engineering» (г. Пермь, 30-31 мая 2012 г. и д. Красновидово, 30 мая-1 июня 2016 г.);

· Международная конференция «A.P. Ershov Informatics Conference» (г. Москва, 27-29 июня 2017 г.);

· Открытая конференция ИСП РАН (г. Москва, 1-2 декабря 2016 г.);

· Международный симпозиум «IEEE East-West Design & Test Symposium» (г. Ереван, Армения, 14-17 октября 2016 г.);

· Всероссийская научно-техническая конференция «Проблемы разработки перспективных микро- и наноэлектронных систем» МЭС-2016 (г. Москва, 3-7 октября 2016 г.);

· Международная конференция «Новые информационные технологии в исследовании сложных структур» (г. Екатеринбург, 6-10 июня 2016 г.);

· Международная летняя школа молодых ученых «Новые информационные технологии в исследовании сложных структур» (г. Анапа, 8-12 июня 2015 г.);

· Научно-техническая конференция студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского (г. Москва, 4 февраля 2015 г.);

· Совместный семинар ЗАО «МЦСТ» и ИСП РАН «Проблемы верификации микропроцессоров» (г. Москва, 10 апреля 2014 г.);

· Семинар Института системного программирования РАН (г. Москва, 2013, 2014 и 2016 гг.).

Публикации

По теме диссертации автором опубликовано 15 работ, в том числе 7 научных статей [1-7] в рецензируемых журналах, входящих в перечень журналов, рекомендованных ВАК РФ. Список опубликованных работ приведен в конце автореферата. В работе [1] дается обзор существующих методов и средств генерации тестовых программ для микропроцессоров. В работах [3, 7, 8, 12, 15] рассказывается о методе конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций. В работе [4] предложен язык описания шаблонов тестовых программ. В работах [6, 14] описывается архитектура расширяемого генератора тестовых программ. В работах [2, 10] приводится описание опыта применения предложенного метода для создания генераторов тестовых программ для архитектуры ARMv8.

Личный вклад

Все представленные в диссертации результаты получены лично автором.

Структура и объем диссертации

Работа состоит из введения, 4 глав, заключения и списка литературы (122 наименования). Основной текст диссертации (без приложений и списка литературы) занимает 120 страниц.

Краткое содержание диссертации

генератор тестовый микропроцессор формальный

Во введении обосновывается актуальность темы работы, определяются ее цели и задачи, раскрывается практическая значимость.

В первой главе дается обзор процесса проектирования микропроцессоров и методов функциональной верификации, применяемых параллельно данному процессу. После этого рассматриваются существующие техники и инструменты генерации тестовых программ. При этом основное внимание уделяется следующим свойствам инструментов генерации:

· Реконфигурируемость - возможность адаптации к тестированию новых микропроцессорных архитектур.

· Расширяемость - возможность интеграции компонентов, реализующих новые техники генерации.

· Контролируемость генерации - возможность контролировать (отражать или отслеживать, предсказывать) текущее состояние микропроцессора (реестров и памяти) в процессе генерации путем исполнения генерируемых последовательностей команд на программном эмуляторе., что позволяет гарантировать корректность построенных программ, создавать самопроверяющие тесты (со встроенными проверками)? и применять техники генерации, использующие информацию о текущем состоянии микропроцессора.

· Систематичность тестирования - возможность систематическим образом обеспечить покрытие интересных для тестирования ситуаций в работе микропроцессора.

Таблица 1 сравнивает возможности существующих генераторов тестовых программ по перечисленным критериям.

Таблица 1. Сравнение возможностей существующих генераторов тестовых программ

На основе сравнительного анализа существующих решений делается вывод об отсутствии генератора тестовых программ, сочетающего все перечисленные выше свойства, и выдвигается тезис об актуальности задачи его создания.

Во второй главе предлагается автоматически конструировать генераторы тестовых программ для микропроцессоров на основе формальных спецификаций их архитектуры. При этом информация, извлеченная из формальных спецификаций, будет использоваться для обеспечения систематичности тестирования и контроля состояния микропроцессора в процессе генерации. Построение тестовых программ будет осуществляться на основе шаблонов, разработанных на специальном расширяемом языке, позволяющем описывать их структурные и поведенческие свойства на высоком уровне абстракции. Расширяемая архитектура генераторов позволит интегрировать разные техники генерации. На рисунке 1 показана схема использования инструмента конструирования генераторов тестовых программ, реализующего предлагаемый метод, и генераторов, построенных с помощью этого инструмента.

Рисунок 1. Схема применения предлагаемого метода

В разделе 2.1 описывается метод автоматизации конструирования генераторов тестовых программ. Предлагается конструировать генераторы тестовых программ для микропроцессоров на основе формальных спецификаций их архитектуры. Спецификации архитектуры взяты за основу, так как при использовании большинства техник генерации требуется информация о синтаксисе и семантике команд. При необходимости спецификации архитектуры могут быть дополнены спецификациями, описывающими особенности микроархитектуры.

Для создания формальных спецификаций архитектуры микропроцессора предлагается использовать язык nML. Спецификации на этом языке включают в себя описания следующих сущностей: типы данных, константы, регистры, режимы адресации, команды и память. Семантика команд задается в виде присваиваний значений переменным, описывающим регистры и память. На рисунке 2 показан пример спецификации команды ADD микропроцессора MIPS64.

Рисунок 2. Спецификация команды ADD архитектуры MIPS64 на nML

Данный пример разработан на основе описания команды в руководстве по архитектуре MIPS64, которое показано на рисунке 3.

Рисунок 3. Описание семантики команды ADD из руководства по архитектуре MIPS64

Язык nML не позволяет описывать логику управления памятью. При обращении к массиву памяти не осуществляется кэширование данных и трансляция адресов, а виртуальный адрес считается равным физическому. Для поддержки генерации тестов для подсистемы управления памятью (MMU, memory management unit) предлагается использовать дополнительные спецификации на языке mmuSL, описывающие механизмы трансляции адресов и кэширования данных.

Далее предлагается конструировать генераторы тестовых программ, состоящие из двух частей: (1) модели, содержащей информацию об архитектуре тестируемого микропроцессора, и (2) ядра, интегрирующего в себе архитектурно-независимые компоненты, реализующие различные техники генерации. При этом ядро является общим для всех конструируемых генераторов. Таким образом, конструирование генератора сводится к построению модели микропроцессора.

Конструируемые генераторы строят тестовые программы на основе шаблонов, задающих их свойства в абстрактном виде. Для создания шаблонов используется специальный язык, позволяющий описывать эти программы в терминах команд, предоставляемых моделью, и техник генерации, поддерживаемых ядром. Обработка тестовых шаблонов заключается в применении компонентов ядра, реализующих техники генерации, к сущностям, определяемым моделью, для построения тестовых программ, обладающих заданными свойствами.

В разделе 2.2 описывается предлагаемый язык описания шаблонов тестовых программ. Данный язык позволяет описывать свойства тестовых программ для любых микропроцессорных архитектур и применять расширяемый набор техник генерации для достижения этих свойств.

В начале раздела описывается структура генерируемых тестовых программ. Они состоят из тестовых воздействий, то есть последовательностей команд, исполнение которых приводит к возникновению некоторых событий в работе микропроцессора, называемых тестовыми ситуациями. Тестовые воздействия предваряются инициализирующим кодом, который подготавливает необходимое начальное состояние микропроцессора. После тестовых воздействий в программы могут добавляться встроенные проверки (self-checks), которые проверяют корректность полученных результатов, сравнивая значения в регистрах и памяти с эталонными. Тестовое воздействие вместе с инициализирующим кодом и встроенными проверками называют тестовым примером (test case). В простейшем случае тестовые примеры не зависят друг от друга и исполняются последовательно. Чтобы обеспечить их исполнение в определенном порядке или параллельное исполнение, в тестовые программы добавляется код диспетчеризации (dispatching code). Кроме этого каждая тестовая программа включает в себя пролог, который осуществляет начальную инициализацию микропроцессора, и эпилог, который завершает работу программы. Таким образом, структуру тестовых программ можно описать формулой

= _start {_{dispatch start}, x_{i, stop}}_{i=1,n stop},

где:

· _start - пролог тестовой программы;

· _dispatch - код диспетчеризации;

· _start, x_{i, stop} - тестовый пример, включающий в себя:

o _start - инициализирующий код;

o x_i - тестовое воздействие;

o _stop - встроенные проверки;

· _stop - эпилог тестовой программы;

· n - число тестовых примеров в программе.

Далее следует описание свойств тестовых программ, задаваемых при помощи шаблонов. На основе одного шаблона можно построить множество тестовых программ, удовлетворяющих описанным свойствам. Это позволяет обеспечить покрытие всевозможных комбинаций тестовых ситуаций. Шаблоны описывают пролог, эпилог и код диспетчеризации в виде фиксированных последовательностей команд, так как выполняемые ими действия могут быть заранее определены. Свойства тестовых примеров описываются следующим образом: задается способ построения последовательностей команд (структурные свойства) и тестовые ситуации, которые должны возникнуть в процессе их исполнения (поведенческие свойства). Свойства тестовых примеров, описываемые при помощи шаблонов, можно разделить на следующие типы:

· способы построения последовательностей команд;

· способы выбора регистров, используемых командами;

· способы комбинирования тестовых ситуаций;

· способы генерации данных для тестовых ситуаций;

· способы построения инициализирующего кода;

· способы построения встроенных проверок.

Для удовлетворения данных свойств применяются разнообразные техники генерации, реализуемые генератором.

Далее описывается предметно-ориентированный язык, который автор предлагает использовать для описания шаблонов тестовых программ. Предлагаемый язык основан на языке Ruby. Использование в качестве основы существующего языка высокого уровня имеет следующие преимущества: (1) все предоставляемые им возможности можно использовать при разработке тестовых шаблонов и (2) изучение языка описания шаблонов становится проще. Ruby был выбран из-за наличия средств метапрограммирования, при помощи которых в язык добавляются конструкции для описания команд тестируемого микропроцессора и директив ассемблера.

Вкратце возможности языка описания шаблонов тестовых программ сводятся к следующему. Шаблон тестовой программы представляет собой Ruby-класс, который реализует методы, внутри которых описываются пролог, эпилог, тестовые примеры и код диспетчеризации. Последовательности команд, составляющие тестовые примеры, описываются в виде блоков, которые можно определять рекурсивно. Отдельный блок представляет собой или элементарный блок или упорядоченный набор вложенных блоков. Атрибуты блоков задают техники генерации, используемые для построения тестовых примеров на основе вложенных элементов. Регистры, используемые командами тестовых примеров, могут задаваться жестко или выбираться по определенным правилам. С командами ассоциируются тестовые ситуации, для которых должны быть сгенерированные тестовые данные. Также в шаблонах определяются правила построения инициализирующего кода и кода встроенных проверок. Выбор конкретных техник генерации (?) определяется значениями атрибутов соответствующих конструкций. Это позволяет наращивать множество поддерживаемых техник без внесения изменений в язык.

На рисунке 4 показано шаблонное описание тестовых примеров, заданных как декартово произведение команд ADD и SUB микропроцессора MIPS, исполнение которых вызывает ситуации Normal и Overflow, и один из вариантов построенного на его основе кода. Используемые регистры выбираются случайным образом и инициализируются в соответствии с правилом, заданным конструкцией preparator.

Рисунок 4. Шаблонное описание и один из тестовых примеров, построенных на его основе

В разделе 2.3 предлагается расширяемая архитектура конструируемых генераторов тестовых программ, которая позволяет интегрировать разные техники генерации.

Генераторы состоят из модели, содержащей информацию об архитектуре тестируемого микропроцессора, и ядра, реализующего архитектурно-независимые техники генерации. Модель включает в себя три основных части: (1) метаданные, хранящие каталог команд, регистров и элементов памяти микропроцессора; (2) эмулятор, позволяющий исполнять команды и получать информацию о состоянии микропроцессора; (3) модель тестового покрытия, содержащая информацию об условиях возникновения тестовых ситуаций, связанных с командами. Взаимодействие с моделью осуществляется через архитектурно-независимые интерфейсы, при этом метаданные используются для обращения к элементам архитектуры. Ядро осуществляет генерацию тестовых программ на основе шаблонов, взаимодействуя с моделью. Процесс генерации включает следующие стадии:

1. Анализ шаблона, в процессе которого строится его абстрактное представление, основанное на метаданных.

2. Построение кода пролога, эпилога и секций диспетчеризации (имеющих фиксированные адреса), а также размещение пролога, секций диспетчеризации и всех глобальных данных в памяти эмулятора. При этом фиксируются адреса тестовых примеров, которые будут размещаться следом за построенными секциями кода.

3. Исполнение построенного кода на эмуляторе с целью подготовки начального состояния, необходимого для генерации тестовых примеров. Исполнение приостанавливается при достижении конца построенного кода.

4. Генерация кода тестового примера, адрес размещения которого был достигнут в процессе исполнения, и размещение его в памяти. В рамках данной стадии выполняются следующие действия:

a. Построение абстрактных последовательности команд.

b. Выбор регистров, используемых командами.

c. Построение комбинаций вариантов решений тестовых ситуаций, связанных с командами.

d. Генерация данных для тестовых ситуаций и построение инициализирующего кода.

5. Запуск исполнения построенного тестового примера на эмуляторе. Исполнение приостанавливается при достижении конечного адреса тестового примера.

6. Построение кода встроенных проверок на основе информации о текущем состоянии регистров и памяти, полученной из эмулятора. При этом построенный код размещается в памяти эмулятора и исполняется.

7. Запуск исполнения с последней точки остановки. При достижении адреса начала еще не построенного тестового примера, выполняется переход к стадии 4. При достижении адреса начала кода диспетчеризации, который еще не был размещен в памяти (адрес не был зафиксирован), он размещается в памяти, а стадия 7 повторяется.

8. Размещение в памяти эмулятора и исполнение эпилога.

9. Печать построенной программы в ассемблерном формате.

Такой подход к генерации тестовых программ дает следующие преимущества: (1) контролируется корректность построенных программ; (2) появляется возможность создавать тесты со встроенными проверками; (3) при построении тестовых примеров учитывается текущее состояние эмулятора.

Ядро включает в себя компоненты, обеспечивающие построение тестовых примеров при помощи различных техник генерации. Эти техники ориентированы на удовлетворение структурных и поведенческих свойств, заданных тестовыми шаблонами. Удовлетворение структурных свойств сводится к построению последовательностей команд определенного вида. Удовлетворение поведенческих свойств заключается в генерации входных данных для команд, которые приводят к возникновению определенных тестовых ситуаций в процессе их исполнения. Поддержка новых техник генерации осуществляется путем добавления соответствующих компонентов.

Основная идея алгоритма построения тестовых примеров заключается в следующем. При помощи различных случайных и комбинаторных техник, реализуемых ядром, строится последовательность команд, описывающая некоторые сценарии работы микропроцессора. После этого осуществляется выбор используемых регистров, за который отвечают реализованные ядром техники выбора регистров. После этого осуществляется генерация входных данных для команд. С командами связаны тестовые ситуации, условия возникновения которых описаны моделью микропроцессора. Эти условия могут иметь разную природу и для их удовлетворения могут использоваться разные техники. Поэтому тестовые ситуации обрабатываются по отдельности. Их обработка происходит в порядке исполнения команд, с которыми они связаны. Способы обработки тестовых ситуаций определяется их типом: для каждого типа тестовой ситуации ядро реализует соответствующую технику.

В третьей главе описывается реализация предложенного метода автоматизации конструирования генераторов тестовых программ. Метод нашел свое воплощение в инструменте с открытым исходным кодом MicroTESK (Microprocessor TEsting and Specification Kit) версии 2.0, разработанном на языке Java. Данный инструмент на основе формальных спецификаций на языках nML и mmuSL конструирует генераторы тестовых программ, состоящие из модели микропроцессора и архитектурно-независимого ядра.

В разделе 3.1 описывается реализации инструмента MicroTESK. Данный инструмент осуществляет построение модели микропроцессора на основе формальных спецификаций и специальных библиотек. Обработка формальных спецификаций осуществляется при помощи транслятора, который поддерживает языки nML и mmuSL, а также позволяет добавить поддержку других языков. Транслятор строит модель путем генерации кода на языке Java. Построенная модель включает в себя метаданные, эмулятор и модель тестового покрытия. Метаданные описывают свойства команд, поддерживаемых тестируемым микропроцессором. Эмулятор отвечает за печать и исполнение команд, описанных при помощи метаданных. Тестовые ситуации, составляющие модель покрытия, описываются в виде ограничений, которые автоматически извлекаются из формальных спецификаций. Транслятор можно расширять дополнительными средствами анализа, позволяющими извлекать новые свойства команд микропроцессора и стоить ограничения новых типов. (строить для них новые типы ограничений).

В разделе 3.2 описывается реализация архитектурно-независимого ядра генераторов тестовых программ. Ядро решает задачи построения внутреннего представления шаблона и генерации тестовых программ на его основе.

Для анализа и построения внутреннего представления шаблонов используется интерпретатор JRuby, который исполняет код на Ruby, взаимодействующий с ядром генератора для конструирования сущностей внутреннего представления. При этом языковые конструкции, позволяющие описывать архитектурно-зависимые сущности, создаются динамически при помощи средств метапрограммирования. Языковые конструкции, связанные с архитектурно-независимыми техниками генерации, реализуются в виде библиотек. Для поддержки новых конструкций требуется разработать дополнительные Ruby библиотеки и компоненты ядра, отвечающие за построение внутреннего представления (чего ?).

Построенное внутреннее представление обрабатывается компонентами ядра, осуществляющими генерацию последовательностей команд и их входных данных. Для каждого типа ограничений, описываемых моделью покрытия, предоставляется компонент, отвечающий за их разрешение. Расширение возможностей генератора достигается путем добавления новых компонентов.

В четвертой главе описываются результаты применения предложенного метода автоматизации конструирования генераторов тестовых программ для микропроцессоров MIPS64, ARMv8, PowerPC и RISC-V. Для данных архитектур были разработаны формальные спецификации системы команд (на языке nML) и подсистемы управления памятью (на языке mmuSL), на основе которых были сконструированы генераторы тестовых программ. Статистика по разработанным спецификациям приводится в таблице 2.

Таблица 2. Статистика по разработанным формальным спецификациям

Практический опыт показал, что трудоемкость разработки формальных спецификаций находится в линейной зависимости от количества команд, поддерживаемых микропроцессором. Трудоемкость описания одной команды зависит от сложности системы команд и в среднем составляет 0.4 человеко-дня. Для сравнения: при использовании инструмента MicroTESK 1.0, который предполагает разработку спецификаций на языке Java, трудоемкость описания одной команды архитектуры MIPS64 составляет около 0.8 человеко-дня. Таким образом, предложенный метод позволяет сократить трудозатраты на создание генератора тестовых программ примерно в 2 раза. Сравнение с другими инструментами генерации не приводится, так как данные о трудоемкости их конфигурирования отсутствуют в открытых источниках.

Разработанные генераторы тестовых программ отвечают основным требованиям, предъявляемым к промышленным инструментам такого рода:

· поддержка различных техник построения тестовых программ (случайные, комбинаторные, на основе ограничений);

· возможность построения самопроверяющих тестов;

· учет архитектурных и микроархитектурных особенностей (условий возникновения исключений, числа вычислительных ядер и потоков, параметров кэш-памяти и т.п.).

Генераторы тестовых программ для MIPS64 и ARMv8 успешно применяются в отечественных и зарубежных компаниях.

В заключении перечисляются основные результаты работы.

Основные результаты работы

Основные научные и практические результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:

1. Разработан метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций.

2. Разработан язык описания шаблонов тестовых программ, позволяющий описывать их структурные и поведенческие свойства на высоком уровне абстракции.

3. Разработана архитектура генераторов тестовых программ для микропроцессоров, позволяющая интегрировать разные техники генерации и допускающая расширение множества поддерживаемых техник.

4. Разработан программный инструмент, реализующий предложенный метод автоматизации конструирования генераторов тестовых программ.

Программный инструмент, реализующий предложенный метод, применяется в промышленных проектах по верификации микропроцессоров.

Работы автора по теме диссертации

1. Татарников А.Д. Обзор методов и средств генерации тестовых программ для микропроцессоров / Татарников А.Д. // Труды ИСП РАН. _ т. 29. _ в. 1. _ 2017. _ С. 167-194.

2. Татарников А.Д. Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK / Камкин А.С., Коцыняк А.М., Проценко А.С., Татарников А.Д., Чупилко М.М. // Труды ИСП РАН. _ т. 28. _ в. 6. _ 2016. _ С. 87-102.

3. Татарников А.Д. Комбинаторная генерация тестовых программ для микропроцессоров на основе формальных спецификаций системы команд / Татарников А.Д. // Сборник трудов конференция «Проблемы разработки перспективных микро- и наноэлектронных систем». _ 2016. _ Часть II. _ C. 38-45.

4. Tatarnikov A. Language for Describing Templates for Test Program Generation for Microprocessors / Tatarnikov A. // Proceedings of the Institute for System Programming. _ Volume 28. _ Issue 4. _ 2016. _ P. 77-98.

5. Татарников А.Д. Средства функциональной верификации микропроцессоров / Камкин А.С., Коцыняк А.М., Смолов С.А., Сортов А.А., Татарников А.Д., Чупилко М.М. // Труды ИСП РАН. _ т. 26. _ в. 1. _ 2014. _ С. 149-200.

6. Татарников А.Д. Расширяемая среда генерации тестовых программ для микропроцессоров / Камкин А.С., Сергеева Т.И., Смолов С.А., Татарников А.Д., Чупилко М.М. // Программирование. _ №1. _ 2014. _ С. 3-14.

7. Tatarnikov A. An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms/ Kamkin A., Protsenko A., Tatarnikov A. // Proceedings of the Institute for System Programming. _ Volume 27. _ Issue 3. _ 2015. _ P. 125-138.

8. Татарников А.Д. Построение поведенческих моделей микропроцессоров для генерации тестовых программ / Татарников А.Д. // Известия высших учебных заведений. Физика. _ Том 59. _ No 8/2. _ 2016. _ С. 97-100.

9. Tatarnikov A. An Approach to Instruction Stream Generation for Functional Verification of Microprocessor Designs / Tatarnikov A. // Proceedings of 14^th IEEE East-West Design & Test Symposium (EWDTS'2016). _ 2016. _ P. 270-273.

10. Tatarnikov A. Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units / Chupilko M., Kamkin A., Kotsynyak A., Protsenko A., Smolov S., Tatarnikov A. // Proceedings of 16^th International Workshop on Microprocessor and SOC Test and Verification (MTV 2015). _ 2015. _ P. 1-7.

11. Татарников А.Д. Генерация тестовых программ для микропроцессоров на основе спецификаций подсистем памяти / Камкин А.С., Проценко А.С., Татарников А.Д. // Известия высших учебных заведений. Физика. _ Том 58. _ No 11/2. _ 2015. _ С. 70-74.

12. Татарников А.Д. Инструмент автоматизации разработки генераторов тестовых программ для микропроцессоров на основе формальных спецификаций / Татарников А.Д. // Материалы научно-технической конференции студентов, аспирантов и молодых специалистов НИУ ВШЭ им. Е.В. Арменского. _ 2015. _ С. 53.

13. Tatarnikov A. Generic Knowledgebase for Test Generation / Kotsynyak A., Tatarnikov A. // Proceedings of SYRCoSE 2014: 8^th Spring/Summer Young Researchers' Colloquium on Software Engineering. _ 2014. _ P. 114-117

14. Tatarnikov A. MicroTESK: An Extensible Framework for Test Program Generation / Kamkin A., Sergeeva T., Tatarnikov A., Utekhin A. // Proceedings of SYRCoSE 2013: 7^th Spring/Summer Young Researchers' Colloquium on Software Engineering. _ 2013. _ P. 51-57.

15. Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors / Kamkin A., Tatarnikov A. // Proceedings of SYRCoSE 2012

Размещено на Allbest.ru