diff Paper/tex/spin_dpp.tex @ 12:3aa9d35e93bf

add conclusion
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 29 Jan 2023 15:21:21 +0900
parents 1a8a9fa534a2
children f0d512637e52
line wrap: on
line diff
--- a/Paper/tex/spin_dpp.tex	Sat Jan 28 23:34:46 2023 +0900
+++ b/Paper/tex/spin_dpp.tex	Sun Jan 29 15:21:21 2023 +0900
@@ -1,3 +1,18 @@
+\chapter{Gears Agda によるモデル検査}
+定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
+できるが,専門的な知識が多く難易度が高いという欠点がある.
+加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
+並列処理を定理証明するには検証する状態が膨大になり困難である。
+そのため、並列処理はモデル検査にて検証する方が良い。
+
+\section{モデル検査とは}
+モデル検査 (Model Cheking) とは、検証手法のひとつである。
+モデル検査はプログラムが入力に対して仕様を満たした動作を
+行うことを網羅的に検証することを指す.
+しかし、モデル検査と定理証明を比較した際に,モデル検査は入力が無限になる
+状態爆発が起こり得るという問題がある.
+実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$  を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。
+
 \section{Dining Philosophers Problem}
 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP)
 を用いることとした.