Инструменты

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

Экспериментальные образцы, созданные в рамках проекта

ЭО ПК МВ

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

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

ЭО ПК АВТ

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

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

Набор инструментов 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.

Ссылки