|
1
|
1 \documentclass[12pt,a4paper,uplatex]{ujreport}
|
|
|
2 \usepackage{master_paper}
|
|
|
3 \usepackage{ascmac}
|
|
|
4 \usepackage[dvipdfmx]{graphicx}
|
|
|
5 \usepackage{here}
|
|
|
6 \usepackage{listings}
|
|
|
7 \usepackage{comment}
|
|
|
8 \usepackage{url}
|
|
|
9 \usepackage[deluxe, multi]{otf}
|
|
|
10 % 以下はハイパーリンク 要ダウンロード
|
|
|
11 \usepackage[dvipdfmx]{hyperref}
|
|
|
12 \usepackage{pxjahyper}
|
|
|
13
|
|
|
14 \usepackage{ascmac}
|
|
|
15 \usepackage[fleqn]{amsmath}
|
|
|
16 \usepackage{amssymb}
|
|
|
17
|
|
|
18 %\input{dummy.tex} %% font
|
|
|
19
|
|
|
20 \jtitle{Gears Agda での形式手法}
|
|
5
|
21 \etitle{Formal Methods in Gears Agda} %
|
|
1
|
22 \year{2023年 3月}
|
|
5
|
23 \eyear{March 2023}
|
|
1
|
24 \author{上地 悠斗}
|
|
|
25 \eauthor{Yuto Uechi}
|
|
|
26 \chife{指導教員：教授 和田 知久}
|
|
|
27 \echife{Supervisor: Prof. Tomohisa Wada}
|
|
|
28
|
|
|
29 \marklefthead{% 左上に挿入
|
|
|
30 \begin{minipage}[b]{.4\textwidth}
|
|
|
31 琉球大学大学院学位論文(修士)
|
|
|
32 \end{minipage}}
|
|
|
33
|
|
|
34 % \markleftfoot{% 左下に挿入
|
|
|
35 % \begin{minipage}{.8\textwidth}
|
|
|
36 % Gears OS の Paging
|
|
|
37 % \end{minipage}}
|
|
|
38
|
|
|
39 \newcommand\figref[1]{図 \ref{fig:#1}}
|
|
|
40 \newcommand\tabref[1]{表 \ref{tab:#1}}
|
|
|
41 \newcommand\coderef[1]{ソースコード \ref{code:#1}}
|
|
|
42
|
|
|
43 \lstset{
|
|
|
44 language=C,
|
|
|
45 tabsize=2,
|
|
|
46 frame=single,
|
|
|
47 basicstyle={\tt\footnotesize}, %
|
|
|
48 identifierstyle={\footnotesize}, %
|
|
|
49 commentstyle={\footnotesize\itshape}, %
|
|
|
50 keywordstyle={\footnotesize\ttfamily}, %
|
|
|
51 ndkeywordstyle={\footnotesize\ttfamily}, %
|
|
|
52 stringstyle={\footnotesize\ttfamily},
|
|
|
53 breaklines=true,
|
|
|
54 captionpos=b,
|
|
|
55 columns=[l]{fullflexible}, %
|
|
|
56 xrightmargin=0zw, %
|
|
|
57 xleftmargin=1zw, %
|
|
|
58 aboveskip=1zw,
|
|
|
59 numbers=left,
|
|
|
60 numberstyle={\scriptsize}, %
|
|
|
61 stepnumber=1,
|
|
|
62 numbersep=0.5zw, %
|
|
|
63 lineskip=-0.5ex,
|
|
|
64 escapechar= \! ,
|
|
|
65 }
|
|
|
66
|
|
|
67 \def\lstlistingname{ソースコード}
|
|
|
68 \def\lstlistlistingname{ソースコード目次}
|
|
|
69
|
|
|
70 % ハイパーリンク
|
|
|
71 \hypersetup{
|
|
|
72 setpagesize=false,
|
|
|
73 bookmarksnumbered=true,%
|
|
|
74 bookmarksopen=true,%
|
|
|
75 colorlinks=true,%
|
|
|
76 linkcolor=black,
|
|
|
77 citecolor=black,
|
|
|
78 }
|
|
|
79
|
|
|
80 %%% 索引のために以下の2行を追加
|
|
|
81 %\usepackage{makeidx,multicol}
|
|
|
82 %\makeindex
|
|
|
83 \begin{document}
|
|
|
84 %rome
|
|
|
85 \maketitle
|
|
5
|
86 \pagenumbering{roman}
|
|
|
87 \setcounter{page}{0}
|
|
1
|
88 \newpage
|
|
|
89
|
|
5
|
90
|
|
1
|
91 \makecommission
|
|
|
92 %\input{chapter/signature.tex}
|
|
|
93
|
|
|
94 \newpage
|
|
|
95
|
|
|
96 %要旨
|
|
|
97 \input{tex/abst.tex}
|
|
|
98
|
|
|
99 %発表履歴
|
|
|
100 \input{tex/history.tex}
|
|
|
101 \addcontentsline{toc}{chapter}{研究関連論文業績}
|
|
|
102
|
|
|
103 \mainmatter
|
|
|
104 %目次
|
|
|
105 \tableofcontents
|
|
|
106
|
|
|
107 %図目次
|
|
|
108 \listoffigures
|
|
|
109
|
|
|
110 %表目次
|
|
|
111 % \listoftables
|
|
|
112
|
|
|
113 %リスト目次
|
|
|
114 \lstlistoflistings
|
|
|
115
|
|
|
116 %chapters
|
|
|
117 \input{tex/intro.tex}
|
|
|
118 \input{tex/cbc.tex}
|
|
|
119 \input{tex/agda.tex}
|
|
|
120
|
|
|
121 \input{tex/cbc_agda.tex}
|
|
|
122
|
|
|
123 \chapter{Gears Agda による定理証明}
|
|
|
124 \input{tex/hoare.tex}
|
|
|
125 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
|
|
|
126 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
|
|
|
127
|
|
|
128 \chapter{Gears Agda によるモデル検査}
|
|
|
129 モデル検査はプログラムが入力に対して仕様を満たした動作を
|
|
|
130 行うことを網羅的に検証することを指す．
|
|
|
131
|
|
|
132 モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
|
|
|
133 状態爆発が起こり得るという問題がある．
|
|
|
134 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
|
|
|
135 できるが，専門的な知識が多く難易度が高いという欠点がある．
|
|
|
136 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
|
|
|
137 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
|
|
|
138 そのため、並列処理はモデル検査にて検証する。
|
|
3
|
139 \section{モデル検査とは}
|
|
|
140 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
|
|
|
141 \section{Gears Agdaによるモデル検査の流れ}
|
|
1
|
142
|
|
5
|
143 % Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い
|
|
|
144
|
|
1
|
145 \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる
|
|
|
146
|
|
|
147 \chapter{今後の展望}
|
|
|
148 ここまでで Gears Agda により定理証明を用いた検証と
|
|
|
149 モデル検査による検証方法を確立した．
|
|
|
150 これからは Red Black Tree の定理証明を用いた検証と，
|
|
|
151 モデル検査部分では現在boundedな検知を行っているので
|
|
|
152 unboundedな検知を行えるようにしたい．
|
|
|
153
|
|
|
154 % %謝辞
|
|
|
155 \input{tex/thanks.tex}
|
|
|
156
|
|
|
157
|
|
|
158 %参考文献
|
|
|
159 \nocite{*}
|
|
|
160 \bibliography{reference}
|
|
|
161 \bibliographystyle{junsrt}
|
|
|
162
|
|
|
163
|
|
|
164 %発表履歴
|
|
|
165 %\addcontentsline{toc}{chapter}{発表履歴}
|
|
|
166 %\input{chapter/history.tex}
|
|
|
167
|
|
|
168 %付録
|
|
|
169 \addcontentsline{toc}{chapter}{付録}
|
|
|
170 \appendix
|
|
|
171 \input{tex/appendix.tex}
|
|
|
172 \end{document}
|
|
|
173
|
|
|
174
|
