Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.tex @ 45:4cecdfd6b237

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 07 May 2020 15:40:54 +0900
parents 698ba8f724d3
children 667ae17b169e
comparison
equal deleted inserted replaced
44:698ba8f724d3 45:4cecdfd6b237
76 76
77 \section{OSの信頼性} 77 \section{OSの信頼性}
78 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。 78 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
79 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。 79 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
80 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。 80 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
81 しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。 81 しかし並列並行処理などに起因するバグや、 そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。
82 また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
83 テスト以外の方法でOSの信頼性を高めたい。 82 テスト以外の方法でOSの信頼性を高めたい。
84 83
85 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 84 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
86 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。 85 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
87 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 86 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。