Технологии создания надежного и безопасного ПО

Добро пожаловать на сайт проекта «Исследование и разработка технологий производства и сертификации программного обеспечения с повышенными требованиями к надежности и безопасности на основе формальных методов моделирования и верификации», проводимого ИСП РАН в партнерстве с АО «НПО РусБИТех» и ФГУП «ГосНИИАС» при поддержке Министерства науки и высшего образования РФ (уникальный идентификатор проекта: RFMEFI60719X0295).

Приглашаем к сотрудничеству организации, заинтересованные в перспективных средствах моделирования, верификации и тестирования ПО.

Цель проекта

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

Ключевые особенности

В настоящее время для поиска ошибок и уязвимостей в ПО (или доказательства их отсутствия) используются разные подходы: статический и статико-динамический анализ; тестирование, в том числе тестирование на основе моделей (model-based testing) и тестирование с имитацией отказов (fault injection); формальная верификация, в том числе дедуктивная верификация и верификация моделей программ (software model checking). Будучи примененными по отдельности (не образуя единой технологической цепочки), эти подходы не обеспечивают должного уровня анализа.

Совместное применение подходов сталкивается с рядом проблем. Во-первых, разные средства обладают разным уровнем технологической зрелости: если инструменты статического анализа уже давно применяются в промышленности, то инструменты дедуктивной верификации еще не вышли за пределы лабораторий. Во-вторых, в разных подходах приняты разные нотации, что усложняет их интеграцию, в частности «сращивание» средств тестирования и формальной верификации. Основная же проблема, на наш взгляд, связана с многоуровневой организацией моделей (что предписывается стандартами ГОСТ 15408 и КТ-178C) – средств анализа ПО на основе многоуровневых моделей в настоящее время нет.

Таким образом, ключевыми особенностями нашего проекта являются:

Научно-технический задел

ИСП РАН проводит исследования в области методов моделирования и верификации ПО с момента своего основания в 1994 году. Наиболее близки к тематике проекта следующие работы института:

Некоторые подходы, разработанные в рамках этих работ, представлены в разделах Материалы и Инструменты.

Материалы

Материалы по моделированию и верификации ПО

Инструменты

Инструменты моделирования и верификации ПО

Публикации

Публикации о моделировании и верификации ПО

Партнеры

Индустриальные и научные партнеры проекта