-
Notifications
You must be signed in to change notification settings - Fork 0
/
common.tex
110 lines (85 loc) · 11.9 KB
/
common.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
% Общие поля титульного листа диссертации и автореферата
\institution{Федеральное государственное бюджетное учреждение науки \\ Институт системного программирования им. В.П.~Иванникова \\ Российской академии наук (ИСП РАН)}
\topic{Методы декомпозиции систем и моделирования окружения программных модулей для верификации Си-программ}
\author{Захаров Илья Сергеевич}
\specnum{05.13.11}
\spec{математическое и программное обеспечение\\
вычислительных машин, комплексов и компьютерных сетей}
\sa{Петренко Александр Константинович}
\sastatus{д.~ф.-м.~н., проф.}
\city{Москва}
\date{\number\year}
\mkcommonsect{objective}{Цели и задачи работы.}{%
{\bf Цель работы} --- развитие методов верификации крупных программных систем на языке программирования Си с использованием инструментов верификации моделей программ при помощи автоматизации декомпозиции системы на модули и синтеза моделей их окружения для сокращения трудоемкости и сроков верификации.
Для достижения поставленной цели были решены следующие задачи:
\begin{enumerate}
\item Исследовать существующие подходы к применению инструментов верификации моделей программ для проверки требований к Си-программам и выявить проблемы, препятствующие расширению применения этих подходов на практике.
\item Разработать архитектуру системы верификации Си-программ, выполняющей генерацию и решение набора верификационных задач при помощи автоматизированной декомпозиции системы на модули и синтеза моделей окружения модулей.
\item Разработать метод автоматизированной декомпозиции Си-программ на модули.
\item Разработать метод автоматизированного синтеза моделей окружения модулей, позволяющий адаптировать процесс синтеза для проверки разных видов требований и программ.
\item Реализовать систему верификации моделей Си-программ на основе разработанных архитектуры и методов, оценить реализацию системы верификации на практике.
\end{enumerate}
}
\mkcommonsect{novelty}{Научная новизна.}{%
Научной новизной обладают следующие результаты работы:
\begin{itemize}
\item Метод автоматизированной декомпозиции Си-программ на модули.
\item Метод спецификации моделей окружения модулей Си-программ на основе композиции систем переходов и доказательство теоремы об изоморфизме множеств достижимых ошибочных состояний спецификации и результата ее трансляции на язык Си.
\item Метод автоматизированного синтеза моделей окружения модулей, позволяющий адаптировать процесс синтеза для проверки разных видов требований и программ.
\end{itemize}
}
\mkcommonsect{method}{Методология и методы исследования.}{%
Результаты диссертации были получены с использованием методов и моделей, применяемых при проведении верификации моделей программ. Математическую основу данной работы составляют теория графов, теория множеств, математическая логика и системы переходов.
}
\mkcommonsect{results}{Положения, выносимые на защиту.}{%
\begin{itemize}
\item Метод автоматизированной декомпозиции Си-программ на модули.
\item Метод спецификации моделей окружения модулей на основе композиции систем переходов.
\item Метод автоматизированного синтеза моделей окружения модулей, позволяющий адаптировать процесс синтеза для проверки разных видов требований и программ.
\end{itemize}
На основе предлагаемых методов была реализована система верификации Klever, предназначенная для проверки требований к программным системам на языке программирования Си с расширениями GNU методом верификации моделей программ. Продемонстрировано, что разработанная архитектура системы верификации позволяет проводить верификацию на различных многоядерных и распределенных вычислительных системах.
}
\mkcommonsect{aprob}{Степень достоверности и апробация результатов.}{%
Основные результаты работы обсуждались на конференциях:
\begin{itemize}
\item 55-я научная конференция МФТИ (г.~Москва, 2012 год).
\item Международная научная конференция студентов, аспирантов и молодых учёных «Ломоносов-2013» (г.~Москва, 2013 год).
\item 7-й весенний/летний коллоквиум молодых исследователей в области
программной инженерии (SYRCoSE, г.~Казань, 2013 год).
\item 10-я конференция разработчиков свободных программ (OSSDEVCONF, г.~Калуга, 2013 год).
\item Международная Ершовская конференция по информатике\linebreak (PSI:~Perspectives of System informatics, г.~ Санкт-Петербург, 2014 год).
\item 5-й международный семинар Linux Driver Verification (г.~Москва, 2015 год).
\item 10-я летняя школа Microsoft Research (г.~Кембридж, Великобритания,
2015 год).
\item 1-й международный семинар, посвященный инструменту CPAchecker \\(г.~Пассау, Германия, 2016 год).
\item 2-й международный семинар, посвященный инструменту CPAchecker \\(г.~Падерборн, Германия, 2017 год).
\item 5-я Международная научно-практическая конференция «Инструменты и методы анализа программ» (г.~Москва, 2017 год).
\item Международная Ершовская конференция по информатике\linebreak (PSI:~Perspectives of System informatics, г.~Москва, 2017 год).
\item 5-я научно-практическая конференция OS DAY (г.~Москва, 2018 год).
\item Научно-практическая открытая конференция ИСП РАН им. В.П.~Иванникова (г.~Москва, 2018 год).
\item Семинар ИСП РАН (г.~Москва, 2018 год).
\end{itemize}
}
\mkcommonsect{pub}{Публикации и зарегистрированные программы.}{%
% Публикации
По теме исследования опубликовано 11 работ \parencite{Syrcose,EnvTrudy,configurable:Trudy,Zakharov2015,ZakharovEnv2015,ZakharovEnvPsi,subsystems:Trudy,survey:new,klever:new,Novikov:2018:ISOLA,Zakharov:2018:ISPRAS} из них 9 в изданиях перечня ВАК~\cite{EnvTrudy,configurable:Trudy,Zakharov2015,ZakharovEnv2015,ZakharovEnvPsi,subsystems:Trudy,survey:new,klever:new,Novikov:2018:ISOLA} и 6 входят в международную систему цитирования Scopus~\cite{Zakharov2015,ZakharovEnv2015,ZakharovEnvPsi,survey:new,klever:new,Novikov:2018:ISOLA}.
В совместных работах~\cite{configurable:Trudy,Zakharov2015} личный вклад автора заключается в описании метода моделирования окружения, а в работах ~\cite{EnvTrudy,ZakharovEnv2015,ZakharovEnvPsi} в описании реализации метода моделирования окружения в системе верификации LDV~Tools.
В совместных работах~\cite{subsystems:Trudy,klever:new,Novikov:2018:ISOLA} личный вклад автора состоит в описании методов декомпозиции программ на модули, а также спецификации и синтеза моделей окружения.
% Патенты
В ходе выполнения работы было получено 4 свидетельства о государственной регистрации программ для ЭВМ:
\begin{enumerate}
\item Свидетельство о государственной регистрации программы для ЭВМ \\№~2015662948: «Программный компонент решения задач верификации посредством использования инфраструктуры облачного сервиса».
\item Свидетельство о государственной регистрации программы для ЭВМ \\{№~2017660773}: «Klever Linux Kernel Verification Objects Generator».
\item Свидетельство о государственной регистрации программы для ЭВМ \\№~2017660774: «Klever Environment Model Generator for Linux Kernel\linebreak Modules».
\item Свидетельство о государственной регистрации программы для ЭВМ \\№~2017660776: «Klever Verification Scheduler».
\end{enumerate}
}
\mkcommonsect{contrib}{Личный вклад автора.}{%
Все представленные в диссертации результаты получены лично автором.
\pagebreak
}
\mkcommonsect{struct}{Структура и объем диссертации.}{%
Диссертация состоит из введения, обзора литературы, 5 глав, заключения и библиографии.
Общий объем диссертации 157 страниц, включая 10 рисунков и 14 таблиц.
Библиография включает 143 наименования на 18 страницах.
}