# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1588144905 -32400
# Node ID a916d03dd4c55c8b264b89bb95dd8d3fc52549e1
# Parent  babdf0b27d62d17cc9105c0b0b625d979643b96f
...

diff -r babdf0b27d62 -r a916d03dd4c5 paper/Makefile
--- a/paper/Makefile	Tue Apr 28 19:21:19 2020 +0900
+++ b/paper/Makefile	Wed Apr 29 16:21:45 2020 +0900
@@ -30,6 +30,9 @@
 
 pdf: $(TARGET).pdf
 
+vi: 
+	vim $(TARGET).tex
+
 
 clean:
 	rm -f *.dvi *.aux *.log  *.ps *.gz *.bbl *.blg *~ *.core
diff -r babdf0b27d62 -r a916d03dd4c5 paper/anatofuz-sigos.pdf
Binary file paper/anatofuz-sigos.pdf has changed
diff -r babdf0b27d62 -r a916d03dd4c5 paper/anatofuz-sigos.tex
--- a/paper/anatofuz-sigos.tex	Tue Apr 28 19:21:19 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Wed Apr 29 16:21:45 2020 +0900
@@ -56,7 +56,12 @@
 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
 しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
 また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
-テストを用いずに別の方法でOSの信頼性を高めたい。
+テスト以外の方法でOSの信頼性を高めたい。
+
+数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
+OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
+これらで信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
+
 
 \nocite{*}
 \bibliographystyle{ipsjunsrt}