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

テストに頼らず定理証明やモデル検査などの形式手法を使用して、OSの信頼性を保証したい。
証明を利用して信頼性を保証する定理証明は、 AgdaやCoqなどの定理証明支援系を利用することになる。
支援系を利用する場合、各支援系でOSを実装しなければならない。
証明そのものは可能であるが、 支援系で証明されたソースコードがそのままOSとして動作する訳ではない。
このためには定理証明されたコードを等価なC言語などに変換する処理系が必要となる。

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

プログラムは本来やりたい計算であるノーマルレベルの計算と、その計算をするのに必要なメタレベルの計算に別けられる。
メタレベルの計算では資源管理などを行うが、 モデル検査などの証明をメタレベルの計算で行いたい。

この実現にはノーマルレベル、メタレベルの計算の処理の切り分けと、メタレベルの計算をより柔軟に扱うOS、言語処理系が必要となる。
両レベルを記述できる言語にContinuation Based (CbC)がある。
CbCはスタック、あるいは環境を持たず継続によって次の処理を行う特徴がある。
CbCを用いて、拡張性と信頼性を両立するOSであるGearsOSを開発している。

GearsOSの開発ではノーマルレベルのコードとメタレベルのコードの両方が必要であり、メタレベルの計算の数は多岐にわたる。
GearsOSの開発を進めていくには、メタレベルの計算を柔軟に扱うAPIや、 自動でメタレベルの計算を作製するGearsOSのビルドシステムが必須となる。
本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察し、言語機能などの拡張を行った。
また、メタ計算を自動生成しているトランスコンパイラを改良し、従来のGearsOSのシステムよりさらに柔軟性が高いものを考案した。
\chapter*{Abstract}
hogefuga