WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 || 3 |

Теорема (об адекватности спецификаций). Пусть инициальный расширенный автомат соответствует контрактной спецификации конвейера, тогда соответствующий спецификационный подавтомат является автоматной моделью конвейера.

Теорема (о полноте спецификаций). Для любой автоматной модели конвейера существует точно описывающая ее контрактная спецификация конвейера.

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

Далее в главе описывается, как контрактные спецификации конвейера могут быть использованы для решения задач тестирования: проверки правильности поведения, оценки полноты тестирования и генерации тестовой последовательности.

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

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

Цель тестирования определяется как покрытие всевозможных обобщенных состояний конвейера — состояний управления, размеченных тестовыми ситуациями и зависимостями. Такие состояния не просто моделируют выполняемые на конвейере операции, но и содержат для каждой из них сведения о тестовой ситуации и информацию о том, как операция зависит от других выполняемых на конвейере операций.

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

Предлагаемый метод генерации тестовой последовательности основан на обходе графа состояний обобщенной автоматной модели конвейера, которая строится на основе управляющего автомата контрактной спецификации конвейера и описания тестового покрытия. Состояниями обобщенной автоматной модели конвейера являются обобщенные состояния, стимулами — стимулы контрактной спецификации конвейера, размеченные тестовыми ситуациями и зависимостями. Показывается, что граф состояний обобщенной автоматной модели конвейера является конечным, детерминированным и сильно-связным, что позволяет применять неизбыточные алгоритмы обхода, исследованные в работах И.Б. Бурдонова, А.С. Косачева, В.В. Кулямина и А.В. Хорошилова.

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

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

В конце главы описывается разработанная автором библиотека PIPE для инструмента CTESK, предназначенная для поддержки создания спецификаций и тестов для модулей с конвейерной организацией.

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

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

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

• предусловие инструкции — определяет ситуации, в которых определено поведение микропроцессора при выполнении данной инструкции. Автоматически создаваемой частью предусловия является проверка совместимости значений входных операндов соответствующим типам данным;

• функция выполнения инструкции — обновляет модельное состояние микропроцессора на основе значений входных операндов инструкции и текущего состояния микропроцессора;

• ассемблерный формат инструкции — определяет формат записи инструкции и ее операндов на языке ассемблера.

Совместно с методом можно использовать два способа проверки правильности поведения: с помощью сравнения трасс и используя тесты со встроенными проверками (self-checking tests). Сравнение трасс основано на ко-симуляции, когда сгенерированные тестовые программы выполняются на тестируемой модели микропроцессора и симуляторе. Результатами выполнения программ являются трассы — последовательности событий, каждое из которых включает данные о выполненной инструкции, значениях ее выходных регистров, состоянии счетчика адреса и, возможно, некоторую другую информацию. Вердикт об ошибке выносится на основе сравнения полученных трасс на соответствие. В случае тестов со встроенными проверками, как видно из названия, проверки правильности поведения вставляются в тестовую программу. Такие тесты можно использовать для тестирования проектных моделей микропроцессоров без использования вспомогательного симулятора, а также для проверки готовых микросхем.

Как и в описанном методе модульного тестирования метод системного тестирования использует неизбыточное описание тестового покрытия в форме тестовых ситуаций и зависимостей. Тестовые ситуации описывают ограничения на значения входных операндов инструкций и состояние микропроцессора. Зависимости ограничивают значения входных операндов для пары инструкций. В методе выделяется два типа зависимостей:

зависимости по регистрам и зависимости по данным. Зависимости по регистрам подразделяются на зависимости типа «определениеиспользование» («чтение после записи»), когда выходной регистр одной инструкции является входным регистром следующей за ней инструкции5, зависимости типа «определение-определение» («запись после записи»), когда выходной регистр одной инструкции также является выходным регистром следующей за ней инструкции, а также зависимости типа «использованиеопределение» («запись после чтения»).

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

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

Генерируемые тестовые программы имеют следующую структуру:

= start {i, xi[si, di]}i=1,n stop, где:

• start — инициализирующая программа префикс тестовой программы, который содержит инструкции, предназначенные для инициализации микропроцессора;

• i, xi[si, di], posti — тестовый вариант (i = 1, …, n):

o i — программа подготовки тестового воздействия последовательность инструкций, осуществляющая инициализацию регистров и памяти микропроцессора;

o xi[si, di] — тестовое воздействие специально подготовленная последовательность инструкций, предназначенная для тестирования микропроцессора, где si — множество тестовых ситуаций, а di — множество зависимостей;

o posti — тестовый оракул последовательность инструкций, содержащая проверку корректности состояния микропроцессора после выполнения тестового воздействия. Тестовый оракул является необязательным элементом тестовой программы.

• stop — завершающая программа постфикс тестовой программы, который содержит инструкции, предназначенные для завершения работы микропроцессора;

• n — размер тестовой программы число тестовых воздействий в программе.

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

• классификация инструкций — инструкции системы команд микропроцессора разбиваются на группы; при генерации указывается максимальное число различных групп инструкций в тестовом воздействии.

• факторизация инструкций — некоторые инструкции внутри одной группы объединяются в классы эквивалентности; тестовые шаблоны, в которых на одинаковых позициях находятся одинаковые инструкции, считаются эквивалентными — для тестирования достаточно использовать любой из них.

• ограничение числа или глубины зависимостей — при генерации указывается максимальное число зависимостей или максимальная глубина зависимостей между инструкциями.

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

В четвертой главе описываются результаты практической апробации предлагаемого автором метода для тестирования промышленных микропроцессоров, их модулей и подсистем, а именно: буфера трансляции адресов, модуля кэш-памяти второго уровня и подсистемы управления памятью микропроцессора Комдив64-СМП, микропроцессора Комдив64 и арифметического сопроцессора Комдив128, разрабатываемых в НИИ системных исследований РАН. Приводятся данные о трудоемкости разработки спецификаций и тестов, объеме разработанных описаний и возможности их повторного использования для тестирования микропроцессоров или их модулей с близкой функциональностью, в частности, для тестирования других версий тех же компонентов. Основным результатом главы является практическое обоснование того, что предлагаемый автором метод автоматизации тестирования микропроцессоров с конвейерной архитектурой соответствует поставленным в работе целям. Обобщенные данные по методам модульного и системного тестирования приведены в таблицах 1 и 2 соответственно.

Таблица 1. Данные по методу модульного тестирования.

Буфер трансляции Модуль кэш-памяти Показатель адресов второго уровня Объем реализации, строк кода 3500 Число тестируемых операций 5 Число требований 99 Объем спецификаций и тестов, 3500 строк кода Трудоемкость разработки 2.5 тестов, чел.-мес.

Число найденных ошибок в 10 проектной модели Таблица 2. Данные по методу системного тестирования.

Подсистема Микропроцессор Сопроцессор Показатель управл. памятью Комдив64 КомдивЧисло тестируемых 4 221 инструкций Объем спецификаций и 5560 47190 тестов, строк кода Трудоемкость разработки 2 9 тестов, чел.-мес.

Число найден. ошибок в 0 6 эталонном симуляторе Число найден. ошибок в 1 9 Нет данных проектной модели Применение метода модульного тестирования в проектах по тестированию буфера трансляции адресов и модуля кэш-памяти второго уровня показывает, что трудоемкость разработки тестов пропорциональна числу требований, накладываемых на тестируемый модуль, и составляет около 2-х требований за 1 человеко-день. Для метода системного тестирования получены данные, что в среднем разработка тестов для 1-ой инструкции микропроцессора занимает 0.7–0.8 человеко-дня. Линейная зависимость трудоемкости разработки тестов от числа требований и инструкций позволяет утверждать, что предлагаемые методы являются масштабируемыми. Данные о трудоемкости разработки тестовых программ для микропроцессора Комдив64-СМП показывают, что предлагаемый метод автоматизации системного тестирования, позволяет сократить затраты на создание системных тестов в 2–2.5 раза.

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

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

Pages:     | 1 || 3 |






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»