--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/anatofuz-sigos.md	Thu Apr 30 13:10:39 2020 +0900
@@ -0,0 +1,21 @@
+# OSの信頼性
+様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
+アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
+OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
+しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
+また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
+テスト以外の方法でOSの信頼性を高めたい。
+
+数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
+OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
+形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
+これに適した形として、 状態遷移モデルが挙げられる。
+OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
+既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。
+分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語で再実装することで仕様の整合性を検証する事が可能である。
+しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。
+実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
+
+実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
+現在小さなunixであるxv6 kernelを状態遷移を基本とした単位でのプログラミングに適した言語、 Continuation Based Cを用いて再実装している。
+再実装の為には、 既存のxv6 kernelの処理の状態遷移を、継続を用いたプログラムに変換していく必要がある。