Глава
MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors
В книге
Генерация тестовых программ на языке ассемблера и проверка корректности результатов их выполнения является наиболее широко применяемым подходом к функциональной верификации микропроцессоров. Данная задача решается при помощи специальных автоматизированных средств, называемых генераторами тестовых программ. Высокая сложность современных электронных устройств создает потребность в автоматизированных средствах, способных генерировать тестовые программы, покрывающие нетривиальные ситуации в их работе. Большинство таких средств используют в качестве входных данных шаблоны тестовых программ, которые позволяют описывать тестовые сценарии в абстрактном виде. Такой подход предоставляет инженерам-верификаторам возможность описывать широкий спектр задач генерации, затрачивая минимальные усилия. Шаблоны тестовых программ разрабатываются на специальных предметно-ориентированных языках. Такие языки должны удовлетворять следующим требованиям: (1) они должны быть достаточно простыми для использования инженерами-верификаторами, не обладающими серьезными навыками программирования; (2) они должны быть применимы для широкого спектра микропроцессорных архитектур и (3) они должны быть легко расширяемы для поддержки описания новых типов задач генерации. В данной работе рассматривается язык описания шаблонов тестовых программ, который был создан для расширяемой среды генерации тестовых программ MicroTESK, разрабатываемой в ИСП РАН. Это гибкий предметно-ориентированный язык, основанный на языке Ruby, который позволяет описывать широкий набор задач генерации в терминах абстракций цифровой аппаратуры. Среда генерации MicroTESK и язык описания тестовых шаблонов успешно применяются в промышленных проектах по верификации микропроцессоров на базе архитектур MIPS и ARM.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации требований (программные контракты и темпоральная логика линейного времени), методы доказательства корректности программ (метод индуктивных утверждений и метод фундированных множеств) и методы проверки моделей (теоретико-автоматный подход в явной и символической формах). В пособии также затрагиваются вопросы абстрактной интерпретации, разрешения ограничений, применения формальных методов в тестировании; даются сведения об инструментах Frama-C и Spin. Каждая глава сопровождается примерами и упражнениями.
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш- ленных микропроцессоров.