Инновации

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

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

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

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

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

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

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

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

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

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

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

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

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

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