Инструменты

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

Набор инструментов AstraVer

Набор инструментов AstraVer, давший название сайту, создан в рамках проекта «Разработка методов и инструментов для дедуктивной верификации модулей ядра операционной системы Linux» (заказчик – Минобрнауки России, 2014-2016 гг.).

Набор инструментов включает в себя платформу анализа исходного кода Frama-C, платформу дедуктивной верификации Why3 и плагин AstraVer платформы Frama-C (развитие плагина Jessie), осуществляющий дедуктивную верификацию Си-программ на соответствие спецификациям на языке ACSL (ANSI C Specification Language) с использованием платформы Why3.

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

Ссылки

Инструмент CTESK

Инструмент CTESK предназначен для автоматизированного тестирования Си-программ. Инструмент реализует технологию UniTESK на платформе языка Си. Для спецификации поведения применяются пред- и постусловия, описанные на языке SeC (Specification extension of C) – расширении языка Си. Тесты генерируются путем обхода графа состояний неявно заданной автоматной модели системы.

Для тестирования сложных систем поддерживается распараллеливание обхода графов состояний на компьютерных кластерах.

Ссылки

Система LDV KLEVER

LDV KLEVER – это конфигурируемая система статической верификации драйверов ядра ОС Linux. Система нацелена на выявление критичных ошибок в драйверах устройств (утечек ресурсов, некорректного использования примитивов синхронизации, недопустимых значений аргументов функций и других). Система, используя модель ядра ОС, подготавливает исходный код драйверов к верификации и проверяет его на соответствие заданным правилам корректности.

Для проверки правил используются такие инструменты, как CPAchecker, BLAST или CBMC.

Ссылки