|
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 での形式手法}
|
|
|
21 \etitle{} %
|
|
|
22 \year{2023年 3月}
|
|
|
23 \eyear{March 2022}
|
|
|
24 \author{上地 悠斗}
|
|
|
25 \eauthor{Yuto Uechi}
|
|
|
26 \chife{指導教員：教授 和田 知久}
|
|
|
27 \echife{Supervisor: Prof. Tomohisa Wada}
|
|
|
28
|
|
|
29
|
|
|
30 \marklefthead{% 左上に挿入
|
|
|
31 \begin{minipage}[b]{.4\textwidth}
|
|
|
32 琉球大学大学院学位論文(修士)
|
|
|
33 \end{minipage}}
|
|
|
34
|
|
|
35
|
|
|
36 % \markleftfoot{% 左下に挿入
|
|
|
37 % \begin{minipage}{.8\textwidth}
|
|
|
38 % Gears OS の Paging
|
|
|
39 % \end{minipage}}
|
|
|
40
|
|
|
41 \newcommand\figref[1]{図 \ref{fig:#1}}
|
|
|
42 \newcommand\tabref[1]{表 \ref{tab:#1}}
|
|
|
43 \newcommand\coderef[1]{ソースコード \ref{code:#1}}
|
|
|
44
|
|
|
45 \lstset{
|
|
|
46 language=C,
|
|
|
47 tabsize=2,
|
|
|
48 frame=single,
|
|
|
49 basicstyle={\tt\footnotesize}, %
|
|
|
50 identifierstyle={\footnotesize}, %
|
|
|
51 commentstyle={\footnotesize\itshape}, %
|
|
|
52 keywordstyle={\footnotesize\ttfamily}, %
|
|
|
53 ndkeywordstyle={\footnotesize\ttfamily}, %
|
|
|
54 stringstyle={\footnotesize\ttfamily},
|
|
|
55 breaklines=true,
|
|
|
56 captionpos=b,
|
|
|
57 columns=[l]{fullflexible}, %
|
|
|
58 xrightmargin=0zw, %
|
|
|
59 xleftmargin=1zw, %
|
|
|
60 aboveskip=1zw,
|
|
|
61 numbers=left,
|
|
|
62 numberstyle={\scriptsize}, %
|
|
|
63 stepnumber=1,
|
|
|
64 numbersep=0.5zw, %
|
|
|
65 lineskip=-0.5ex,
|
|
|
66 escapechar= \! ,
|
|
|
67 }
|
|
|
68
|
|
|
69 \def\lstlistingname{ソースコード}
|
|
|
70 \def\lstlistlistingname{ソースコード目次}
|
|
|
71
|
|
|
72 % ハイパーリンク
|
|
|
73 \hypersetup{
|
|
|
74 setpagesize=false,
|
|
|
75 bookmarksnumbered=true,%
|
|
|
76 bookmarksopen=true,%
|
|
|
77 colorlinks=true,%
|
|
|
78 linkcolor=black,
|
|
|
79 citecolor=black,
|
|
|
80 }
|
|
|
81
|
|
|
82 %%% 索引のために以下の2行を追加
|
|
|
83 %\usepackage{makeidx,multicol}
|
|
|
84 %\makeindex
|
|
|
85 \begin{document}
|
|
|
86 %rome
|
|
|
87 \maketitle
|
|
|
88
|
|
|
89 \newpage
|
|
|
90
|
|
|
91 \pagenumbering{roman}
|
|
|
92 \setcounter{page}{0}
|
|
|
93 \makecommission
|
|
|
94 %\input{chapter/signature.tex}
|
|
|
95
|
|
|
96 \newpage
|
|
|
97
|
|
|
98 %要旨
|
|
|
99 \input{tex/abst.tex}
|
|
|
100
|
|
|
101 %発表履歴
|
|
|
102 \input{tex/history.tex}
|
|
|
103 \addcontentsline{toc}{chapter}{研究関連論文業績}
|
|
|
104
|
|
|
105 \mainmatter
|
|
|
106 %目次
|
|
|
107 \tableofcontents
|
|
|
108
|
|
|
109 %図目次
|
|
|
110 \listoffigures
|
|
|
111
|
|
|
112 %表目次
|
|
|
113 % \listoftables
|
|
|
114
|
|
|
115 %リスト目次
|
|
|
116 \lstlistoflistings
|
|
|
117
|
|
|
118 %chapters
|
|
|
119 \input{tex/intro.tex}
|
|
|
120 \input{tex/cbc.tex}
|
|
|
121 \input{tex/agda.tex}
|
|
|
122
|
|
|
123 \input{tex/cbc_agda.tex}
|
|
|
124
|
|
|
125 \chapter{Gears Agda による定理証明}
|
|
|
126 \input{tex/hoare.tex}
|
|
|
127 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
|
|
|
128 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
|
|
|
129
|
|
|
130 \chapter{Gears Agda によるモデル検査}
|
|
|
131 モデル検査はプログラムが入力に対して仕様を満たした動作を
|
|
|
132 行うことを網羅的に検証することを指す．
|
|
|
133
|
|
|
134 モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる
|
|
|
135 状態爆発が起こり得るという問題がある．
|
|
|
136 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
|
|
|
137 できるが，専門的な知識が多く難易度が高いという欠点がある．
|
|
|
138 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
|
|
|
139 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
|
|
|
140 そのため、並列処理はモデル検査にて検証する。
|
|
3
|
141 \section{モデル検査とは}
|
|
|
142 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
|
|
|
143 \section{Gears Agdaによるモデル検査の流れ}
|
|
1
|
144
|
|
|
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
|
