Инновации

AstraVer Toolset: система верификации ключевых компонентов

AstraVer Toolset – система дедуктивной верификации ключевых компонентов. Позволяет разрабатывать и верифицировать модели политик безопасности, а также проводить доказательство корректности компонентов на языке С. Необходимый инструмент достижения целей семейств доверия ADV_SPM и ADV_FSP, определённых в ГОСТ Р ИСО/МЭК 15408-3-2013.

Klever: система автоматической статической верификации Си-программ

Klever – система верификации, которая автоматически строит модели на основе исходного кода на языке программирования Си. Klever позволяет специфицировать различные требования по безопасности и надёжности, а также проверять их выполнение автоматически с заданным уровнем точности. В основе системы верификации лежат методы для покомпонентной верификации, моделирования окружения и спецификации требований, что делает возможным применение формальных методов к исходному коду размером в сотни тысяч и миллионы строк.

Masiw: поддержка проектирования ответственных систем

MASIW – набор инструментов для разработки программно-аппаратных комплексов ответственных систем в сфере авиации, медицины и др. Создан для инженеров-конструкторов комплексов бортового оборудования для авиационных судов, разрабатываемого с применением интегрированной модульной авионики (ИМА). Оперативно адаптируется под другие предметные области.

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

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

TestOS: окружение для тестирования ПО

TestOS — окружение для модульного тестирования программного обеспечения на целевой аппаратуре. Позволяет проводить отработку программного обеспечения для ответственного применения в целях выполнения сертификационных и иных мероприятий на архитектурах AArch64, ARM, PowerPC, MIPS, RISC-V и x86.

Requality: инструмент управления требованиями

Requality – расширяемый инструмент для управления требованиями. Позволяет как разрабатывать требования к проектируемым системам с нуля, так и формировать каталоги требований путём разметки существующих документов, сохраняя при этом связи между требованиями и текстовыми фрагментами исходных документов. Поддерживает организацию иерархической структуры требований, трассируемость между требованиями разных уровней, возможность совместной работы над требованиями с использованием системы управления версиями GIT.

Retrascope: инструмент статического анализа hdl-описаний

Retrascope – инструмент функциональной верификации модулей цифровой аппаратуры. Retrascope предоставляет автоматизированные средства анализа кода, извлечения формальных моделей и генерации функциональных тестов. В качестве входных данных инструмент принимает описания модулей цифровой аппаратуры на синтезируемых подмножествах языков Verilog и VHDL, а также спецификации поведения.