changeset 6:a916d03dd4c5

...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Wed, 29 Apr 2020 16:21:45 +0900
parents babdf0b27d62
children 8f1d03a81516
files paper/Makefile paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 3 files changed, 9 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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
Binary file paper/anatofuz-sigos.pdf has changed
--- 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}