Этап 3

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

  1. Разработка метода генерации условий верификации для программ, работающих с разделяемыми данными.
  2. Разработка алгоритмов генерации условий верификации для программ, работающих с разделяемыми данными.
  3. Участие в мероприятиях, направленных на освещение и популяризацию промежуточных и окончательных результатов ПНИ.
  4. Разработка тестовых модулей, верификация которых не требует учёта работы с разделяемыми данными, с целью обеспечения экспериментальных исследований реалистичными тестовыми программами.
  5. Проведение маркетинговых исследований.

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

В результате проведённых работ были разработаны метод и алгоритмы генерации условий верификации для программ, работающих с разделяемыми данными. На следующем этапе ПНИ запланирована реализация этих алгоритмов в виде экспериментального образца системы дедуктивной верификации компонентов операционных систем, а также подача заявки на регистрацию программы ЭВМ в Патентное Ведомство России с целью регистрации результатов интеллектуальной деятельности.

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

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

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

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