Проекты

Summer — система разработки тестов на основе автоматных моделей

Summer — система разработки тестов на основе автоматных моделей, поддерживающая технологию UniTESK.

Разработка тестовых наборов для математических библиотек

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

Linux Driver Verification (LDV)

Программа Linux Driver Verification (LDV) объявлена Центром верификации ОС Linux в июне 2009 года.

Технология тестирования интеграции в крупных информационных системах

Проект ведется в партнерстве с ОАО "Вымпелком" и нацелен на развитие методов тестирования на уровне информационной системы вцелом. Проект охватывает самые разные аспекты процесса тестирования: от сбора требований к legacy-системам до анализа тестового покрытия при end-to-end тестировании.

UniTESK

UniTESK - это технология тестирования программных интерфейсов (API), которая в первую очередь предназначена для модульного тестирования. Название UniTESK расшифровывается как Unified TEsting Specification based toolKit (Унифицированный набор инструментов для тестирования на основе спецификаций). Унифицированность UniTESK обеспечивается тем, что общая методология тестирования и общая архитектура может быть реализована для тестирования модулей на практически всех языках программирования. В настоящее время имеются реализации UniTESK для C (CTESK), C++ (C++TESK), Java (JavaTESK и Summer), Python (PyTESK).

Retrascope: инструмент обратной инженерии HDL-описаний

HDL Retrascope — это инструмент обратной инженерии (reverse engineering) и трансформаций (transformation) описаний цифровой аппаратуры, выполненных на таких HDL-языках (hardware description languages), как Verilog и VHDL. Инструмент позволяет анализировать HDL-описания, реконструировать, лежащие в их основе модели (расширенные конечные автоматы), и использовать полученные модели для генерации тестов, проверки свойств и других задач.

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

MicroTESK (Microprocessor TEsting and Specification Kit) — это среда генерации тестовых программ на языке ассемблера для функциональной верификации микропроцессоров. В качестве источника знания о конфигурации верифицируемого микропроцессора выступают формальные спецификации. Задачи генерации описываются на специальном языке, основанном на Ruby, который позволяет формулировать цели верификации в терминах тестовых ситуаций, извлеченных из формальных спецификаций. Такой подход позволяет упростить настройку среды и повысить уровень тестового покрытия. MicroTESK успешно применяется в промышленных проектах по верификации микропроцессоров ARMv8 и MIPS64.

MASIW. Программные средства поддержки проектирования комплексов бортового оборудования

Автоматизированное рабочее место архитектора и интегратора системы интегрированной модульной авионики (ИМА) предназначено для автоматизации процесса проектирования комплексов бортового оборудования (КБО).

LDV. Технология статической верификации драйверов ядра ОС Linux

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

AstraVer Toolset: инструменты дедуктивной верификации моделей и механизмов защиты ОС

Сбои в программном обеспечении (ПО) ответственных систем, таких как, системы защиты информацией, системы управления самолётом или опасным производством, могут привести к неприятным и даже катастрофическим последствиям. По этой причине разработка такого ПО находится под контролем сертифицирующих органов, которые требуют применения лучших практик, закреплённых в международных стандартах (DO-178С, ISO/IEC 15408 и т.д.).

Разработка с использованием инструмента C++TESK системы функциональной верификации кэш-памяти третьего уровня проекта "Процессор 1"

Целью данного проекта являлась разработка с использованием технологии UniTESK и инструмента C++TESK системы функциональной верификации (тестовой системы) для кэш-памяти третьего уровня (L3) проекта «Процессор 1», а также проведение верификации с использованием разработанной тестовой системы.

Разработка с использованием инструмента C++TESK систем автономной функциональной верификации устройств L3 и DB проектов "Процессор 1" и "Процессор 2"

Целью данного проекта являлась разработка с использованием технологии UniTESK систем автономной функциональной верификации (тестовых систем) для устройств проектов «Процессор 1» и «Процессор 2», доработка (приведение в актуальное состояние и расширение возможностей) существующих тестовых систем, а также проведение верификации с использованием разработанных заново и доработанных тестовых систем.

Разработка инфраструктуры стандарта LSB

Программа LSB Infrastructure выполнялась ИСП РАН по контракту с Linux Foundation. Проект был начат в сентябре 2006 и был нацелен на долгосрочное сотрудничество с целью поднятия на новый уровень инфраструктуры разработки и поддержки стандарта LSB в ответ на возрастающую потребность индустрии в продвижении этого стандарта.