brand

MicroTESK: генератор тестовых программ

Скачать сборник технологий

MicroTESK: генератор тестовых программ

MicroTESK – реконфигурируемая и расширяемая среда генерации тестовых программ для функциональной верификации микропроцессоров и виртуальных машин. Позволяет автоматически конструировать генераторы тестовых программ на основе формальных спецификаций систем команд. MicroTESK применим для широкого спектра архитектур (RISC, CISC, стековые и регистровые виртуальные машины).

Особенности и преимущества

MicroTESK – комплекс инструментов, включающий в себя средства моделирования (построение модели тестируемой системы по формальным спецификациям) и средства генерации (построение тестовых программ по шаблонам). Распространяется по лицензии Apache 2.0. MicroTESK доступен на сайте ИСП РАН: https://forge.ispras.ru/projects/microtesk. Описание технологии − на сайте http://www.microtesk.org.

MicroTESK – это:

  • Использование формальных спецификаций в качестве источников знаний об устройстве тестируемой системы:
    • спецификации системы команд на nML (регистры, память и режимы адресации, логика инструкций, текстовый/двоичный формат инструкций);
    • дополнительные спецификации подсистемы памяти на mmuSL (свойства буферов памяти (TLB, L1 и L2), логика трансляции адресов и логика операций чтения и записи);
  • Генерация тестовых программ на основе объектно-ориентированных тестовых шаблонов:
    • тестовые шаблоны на языке Ruby (описывают способ построения цепочек инструкций и тестовых данных, допускают повторное использование);
    • возможность использования разных техник генерации цепочек инструкций и тестовых данных (случайная генерация, комбинаторная генерация, генерация на основе ограничений);
  • Широкий набор поддерживаемых архитектур микропроцессоров:
    • RISC и CISC (разработаны генераторы тестовых программ для таких архитектур, как RISC-V, ARM, MIPS, PowerPC);
    • регистровые и стековые архитектуры виртуальных машин;
    • многоядерность/многопоточность системы.

    • Системные требования

    Java 11, ОС Windows или ОС на базе ядра GNU/Linux.

    Опыт внедрения

    MicroTESK разрабатывается с 2007 года. Использовался в российских и международных проектах по разработке современных индустриальных микропроцессоров и виртуальных машин (в частности, в промышленных проектах по верификации микропроцессоров ARMv8, MIPS64, RISC-V и виртуальной машины Ark).

    Схема работы

    Генератор тестовых программ MicroTESK

    Рис. 1. Традиционная генерация тестовых программ.

    Разработчик/участник

    Технологии программирования

    Перейти к списку всех технологий