# HG changeset patch # User anatofuz # Date 1588833654 -32400 # Node ID 4cecdfd6b2374c955a467eb0f0a4a43c948ac106 # Parent 698ba8f724d3a21b05e9996384d696ab2254bf8e update diff -r 698ba8f724d3 -r 4cecdfd6b237 paper/anatofuz-sigos.md --- a/paper/anatofuz-sigos.md Thu May 07 11:05:55 2020 +0900 +++ b/paper/anatofuz-sigos.md Thu May 07 15:40:54 2020 +0900 @@ -2,8 +2,7 @@ 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。 -しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。 -また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。 +しかし並列並行処理などに起因するバグや、 そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 テスト以外の方法でOSの信頼性を高めたい。 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 diff -r 698ba8f724d3 -r 4cecdfd6b237 paper/anatofuz-sigos.pdf Binary file paper/anatofuz-sigos.pdf has changed diff -r 698ba8f724d3 -r 4cecdfd6b237 paper/anatofuz-sigos.tex --- a/paper/anatofuz-sigos.tex Thu May 07 11:05:55 2020 +0900 +++ b/paper/anatofuz-sigos.tex Thu May 07 15:40:54 2020 +0900 @@ -78,8 +78,7 @@ 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。 -しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。 -また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。 +しかし並列並行処理などに起因するバグや、 そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 テスト以外の方法でOSの信頼性を高めたい。 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。