Mercurial > hg > Papers > 2020 > anatofuz-sigos
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
--- 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}