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


Инновации

Собственные технологии

Система верификации AstraVer Toolset

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

Klever: система верификации моделей промышленного программного обеспечения

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

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

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

MicroTESK: среда генерации тестовых программ для микропроцессоров

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

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

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