Этап 1

В ходе выполнения проекта по Соглашению о предоставлении субсидии от 27.06.2014 №14.604.21.0051 с Минобрнауки России в рамках федеральной целевой программы «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2014-2020 годы» на этапе №1 в период с 27.06.2014 по 31.12.2014 выполнялись следующие работы:

  1. Аналитический обзор современной научно-технической литературы.

  2. Проведение патентных исследований в соответствии с ГОСТ 15.011-96.

  3. Исследование методов дедуктивной верификации программ и направлений их развития для верификации компонентов операционных систем.

  4. Участие в мероприятиях, направленных на освещение и популяризацию промежуточных и окончательных результатов ПНИ.

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

  6. Анализ потребностей рынка в инструментах дедуктивной верификации.

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

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

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

Полученные научные и научно-технические результаты соответствуют техническим требованиям к выполняемому проекту, заданным в техническом задании.

Комиссия Минобрнауки России признала обязательства по Соглашению на отчетном этапе исполненными надлежащим образом.