\chapter*{要旨}
アプリケーションの信頼性を保証するには、土台となるOSの信頼性は高く保証されていなければならない。
信頼性を保証する方法としてテストコードを使う手法が広く使われている。
OSのソースコードは巨大であり、並列処理など実際に動かさないと発見できないバグが存在する。
OSの機能をテストですべて検証するのは不可能である。

テストに頼らず定理証明やモデル検査などの形式手法を使用して、OSの信頼性を保証したい。
証明を利用して信頼性を保証する定理証明は、 AgdaやCoqなどの定理証明支援系を利用することになる。
支援系を利用する場合、各支援系でOSを実装しなければならない。
証明そのものは可能であるが、 支援系で証明されたソースコードがそのままOSとして動作する訳ではない。
証明されたコードと、実際に動作するOSを記述するC言語などのプログラミング言語の間にはギャップが存在する。
Cでの実装時に入るバグは取り除けない。
このためには定理証明されたコードを等価なC言語などに変換する処理系が必要となる。

信頼性を保証するほかの方法として、プログラムの可能な実行をすべて数え上げて仕様を満たしているかを確認するモデル検査がある。
モデル検査は実際に動作しているプログラムに対して実行することが可能である。


\chapter*{Abstract}
hogefuga