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

В настоящее время большой популярностью пользуются языки программирования, использующие в своей инфраструктуре языковые виртуальные машины (ВМ), что стимулирует развитие данной технологии. Разработка языковой ВМ – сложный процесс, в ходе которого могут вноситься ошибки в проектируемую систему. Для обеспечения качества реализации ВМ процесс разработки включает в себя этап тестирования. При тестировании необходимо ответить на два основных вопроса: как создавать тестовые программы и как проверять результат их исполнения. В статье представлен метод функционального тестирования языковых ВМ на основе формальных спецификаций системы команд. В работе описана реализация предложенного подхода. На основе документации ВМ специфицируется системы команд с помощью языка описания архитектуры. На основе спецификации системы команд строится исполнимая модель. Для автоматизации создания тестовых программ используются тестовые шаблоны – параметризованные описания тестовых программ. При создании тестовых шаблонов используется специальный предметно-ориентированный язык, позволяющий задавать различные техники генерации и использовать байт-код ВМ, полученный из формальных спецификаций. В представленном методе тестовые шаблоны могут быть описаны вручную, сгенерированы автоматически, в соответствии с целевым критерием, или получены от сторонних генераторов. На основе тестовых шаблонов и исполнимой модели генерируются тестовые программы на байт-коде, нацеленные на проверку определенной функциональности или свойств тестируемой системы. Байт-код является естественным языком для ВМ и позволяет воздействовать на всю ее функциональность. Тестовая программа транслируется в бинарную программу и исполняется на ВМ. Во время исполнения программы на ВМ собирается трасса исполнения. Для анализа трассы исполнения создается адаптер трасс. На основе исполнимой модели и адаптера трасс строится тестовый оракул. Оракул проверяет результаты тестирования путем сравнения трассы исполнения с результатами исполнения бинарной программы на исполнимой модели. Метод реализован в инструменте MicroTESK версии 2.6 и был использован для тестирования ВМ Ark.