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

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

Стадии проекта
Предложение принято
Конкурс завершен
Проект закончен
Проект
14.604.21.0051
Организация
ИСП РАН

Создание новой продукции и технологий с целью создания конкретного образца (типа изделия, материала) или исследования особенностей его функционирования или применения

Этапы проекта

1
27.06.2014 - 31.12.2014
Подготовлен список статей для анализа и выполнен обзор 10 статей из него. Выполнен поиск и отбор патентов по ключевым словам: дедуктивная верификация, верификация операционных систем, аналитическая верификация. Проведены эксперименты с несколькими доступными инструментами: Frama-C, Why3, WP. Проведены опросы потенциальных пользователей относительно потребностей в инструментах верификации.
Развернуть
2
01.01.2015 - 30.06.2015
Разработка метода генерации моделей памяти компонентов операционных систем с возможностью интерпретации участков памяти как объектов разных типов.
  Разработка алгоритмов генерации моделей памяти компонентов операционных систем с возможностью интерпретации участков памяти как объектов разных типов.
  Разработка метода генерации моделей памяти разделяемой между несколькими потоками управления.
Разработка алгоритмов генерации моделей памяти разделяемой между несколькими потоками управления.
Развернуть
3
01.07.2015 - 31.12.2015
Разработаны методы и алгоритмы генерации моделей памяти компонентов операционных систем с возможностью интерпретации участков памяти как объектов разных типов. Разработаны методы и алгоритмы генерации моделей памяти, разделяемой между несколькими потоками управления. Разработаны методы и алгоритмы генерации условий верификации для программ, работающих с разделяемыми данными. Идентифицированы и описаны распространённые дисциплины синхронизации при работе с разделяемыми данными в компонентах операционных систем Индустриального партнёра в обеспечение разработки метода генерации условий верификации для программ, работающих с разделяемыми данными. Разработаны тестовые модули, верификация которых не требует учёта работы с разделяемыми данными.
Развернуть
4
01.01.2016 - 30.06.2016
Разработан экспериментальный образец системы дедуктивной верификации компонентов операционных систем. Разработаны программы и методики экспериментальных исследований экспериментального образца системы дедуктивной верификации компонентов операционных систем.
Развернуть
5
01.07.2016 - 31.12.2016
Разработан экспериментальный образец системы дедуктивной верификации компонентов операционных систем. Разработан проекта технического задания на ОКР.
Развернуть

Программа

Программа "Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2014-2020 годы"

Программное мероприятие

1.2 Проведение прикладных научных исследований для развития отраслей экономики
Продолжительность работ
2014 - 2016, 30 мес.
Бюджетные средства
25 млн
Организация
ФТИ им. А.Ф.Иоффе
профинансировано
Тема
Конкурсный отбор двухлетних прикладных научных исследований, направленных на создание продукции и технологий, по приоритетному направлению "Науки о жизни" в рамках мероприятия 1.2 Программы.
Продолжительность работ
2014 - 2015, 18 мес.
Бюджетные средства
300 млн
Количество заявок
85
Тема
Конкурсный отбор трехлетних прикладных научных исследований, направленных на создание продукции и технологий, по приоритетному направлению "Науки о жизни" в рамках мероприятия 1.2 Программы.
Продолжительность работ
2014 - 2016, 30 мес.
Бюджетные средства
780 млн
Количество заявок
233
Тема
Конкурсный отбор двухлетних прикладных научных исследований, направленных на создание продукции и технологий, по приоритетному направлению «Индустрия наносистем» в рамках мероприятия 1.2 Программы.
Продолжительность работ
2014 - 2015, 18 мес.
Бюджетные средства
300 млн
Количество заявок
105
Тема
Конкурсный отбор трехлетних прикладных научных исследований, направленных на создание продукции и технологий, по приоритетному направлению «Индустрия наносистем» в рамках мероприятия 1.2 Программы.
Продолжительность работ
2014 - 2016, 30 мес.
Бюджетные средства
780 млн
Количество заявок
249
Тема
Конкурсный отбор двухлетних прикладных научных исследований, направленных на создание продукции и технологий, по приоритетному направлению «Информационно-телекоммуникационные системы» в рамках мероприятия 1.2 Программы.
Продолжительность работ
2014 - 2015, 18 мес.
Бюджетные средства
200 млн
Количество заявок
87