10.12.2019: Начало проекта по методам моделирования и верификации программного обеспечения

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

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

Презентация проекта и первые результаты были представлены на выставке технологий ИСП РАН, проводимой в рамках Открытой конференции ИСП РАН им. В.П. Иванникова. На ней был продемонстрирован набор инструментов AstraVer, предназначенный для дедуктивной верификации компонентов ПО ответственного назначения. AstraVer позволяет разрабатывать и верифицировать модели политик безопасности, а также проводить доказательство корректности модулей на языке С. Основное внимание уделялось разработанным в рамках проекта новым методам и проектам инструментов, ориентированным на использование многоуровневых моделей для верификации и тестирования ПО.

За результатами выполнения проекта можно следить на сайте astraver.linuxtesting.org.