Регистрация / Вход
Прислать материал

Разработка методов и инструментов для масштабируемой статической верификации системного программного обеспечения.

Номер контракта: 14.616.21.0015

Руководитель: Петренко Александр Константинович

Должность: Заведующий отделом

Организация: Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В.П. Иванникова Российской академии наук
Организация докладчика: Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук

Аннотация скачать
Постер скачать
Ключевые слова:
системное программное обеспечение, анализ программ, верификация моделей программ, статическая верификация, регрессионная верификация, формальная спецификация, формальный метод.

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

Основные планируемые результаты проекта:
При выполнении прикладных научных исследований будут получены следующие результаты:
- отчет о прикладных научных исследованиях;
- отчет о патентных исследованиях;
- метод параллельной статической верификации системного программного обеспечения;
- метод фильтрации трасс ошибок, позволяющий выявлять несколько ошибок в программном обеспечении;
- метод оценки покрытия исходного кода при статической верификации;
- метод статической верификации многопоточного программного обеспечения;
- экспериментальный образец программного комплекса масштабируемой статической верификации системного программного обеспечения (ЭО ПК);
- программная документация ЭО ПК;
- программа и методики экспериментальных исследований ЭО ПК;
- проект технического задания на проведение ОКР по теме: «Разработка инструментов для масштабируемой статической верификации промышленного системного программного обеспечения»;
- метод повторного использования результатов статической верификации, получаемых на различных этапах анализа программного обеспечения;
- метод подготовки снимка состояния инструмента статической верификации, позволяющий проверять различные части программного обеспечения независимым образом;
- метод визуализации трасс ошибок различных инструментов статической верификации;
- метод верификации программного обеспечения, использующего операции с числами с плавающей точкой;
- метод сертификации результатов статической верификации программного обеспечения.
Разрабатываемые методы статического анализа позволят сократить время, требуемое на верификацию, повысить ее качество и сократить усилия экспертов на анализ результатов.

Краткая характеристика создаваемой/созданной научной (научно-технической, инновационной) продукции:
Конечным продуктом является программный комплекс масштабируемой статической верификации системного программного обеспечения, который позволит обойти ограничения по размеру и сложности верифицируемого программного обеспечения, а также поможет развитию международной кооперации в научных исследованиях.
Разрабатываемые методы параллельной верификации и методы проверки одновременно нескольких правил корректности позволят снизить требуемое для анализа время. Методы повторного использования результатов статической верификации и метод подготовки снимка состояний инструментов снизят требования к ресурсам при анализе большого объема кода. Данные методы имеют общие черты с хорошо известными подходами - условной верификацией (conditional model checking) и регрессионной верификацией (regression verification).
Для достижения поставленных целей будет создан экспериментальный образец программного комплекса. Он будет исследован согласно разработанной методике экспериментальных исследований на предмет соответствия техническому заданию.

Назначение и область применения, эффекты от внедрения результатов проекта:
Разработка нового метода масштабируемой статической верификации системного программного обеспечения позволит получить новые значимые научные результаты, превосходящие мировой уровень.
В практической плоскости областью применения полученных результатов является верификация всех видов программного обеспечения, написанного на языке Си, в первую очередь, системного программного обеспечения.
В учебном и в методическом плане, результаты проекта могут использоваться в учебных курсах и тренингах, посвященных современным методам статической верификации. Все разработки, которые планируются в рамках проекта, будут публиковаться под открытой лицензией, что позволит всем исследователям и преподавателям использовать результаты проекта.

Текущие результаты проекта:
В 2015 году были разработаны методы фильтрации трасс ошибок, позволяющие проверять несколько правил корректности за один запуск инструмента статической верификации и метод параллельной статической верификации системного программного обеспечения, позволяющий проверять одновременно несколько правил корректности.
Иностранный партнер (Университет Пассау) разработал метод подготовки снимка состояния инструмента статической верификации, позволяющий проверять различные части программного обеспечения независимым образом.
Разработанные методы позволяют существенно снизить требования к ресурсам при верификации системного программного обеспечения, а также повышают удобство использования экспертами.