# HG changeset patch # User anatofuz # Date 1574308282 -32400 # Node ID 1a881e24e43827eff31c4e93284f5c3760a54788 # Parent 450d0e91835b932497dcc819b8d881fd7f8349fb tweak diff -r 450d0e91835b -r 1a881e24e438 paper/anatofuz_prosym_2019.pdf Binary file paper/anatofuz_prosym_2019.pdf has changed diff -r 450d0e91835b -r 1a881e24e438 paper/anatofuz_prosym_2019.tex --- a/paper/anatofuz_prosym_2019.tex Thu Nov 21 12:40:00 2019 +0900 +++ b/paper/anatofuz_prosym_2019.tex Thu Nov 21 12:51:22 2019 +0900 @@ -64,10 +64,11 @@ 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。 頻繁に並列処理を行うOSでは、 スレッド間の共通資源の競合などの非決定的な実行を行う。 OSの信頼性を保証する上ではテストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。 -そのため、 テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。 -しかしOSの殆どはC言語やアセンブラで記述されており、 これらでは関数呼び出し時で実行する処理にスタックに積まれた変数や、 グローバル変数などを多様してしまう。 +テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。 +そのためには定理証明支援系などで証明が可能な形式と、 等価な形式でOSを記述する必要性がある。 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。 - +CbCは状態遷移単位での実行であり、 他の状態に遷移する際に今までの環境を持たない。 +そのため、 CbCで実装した処理は入出力が明確化され、 定理証明支援系で表現可能な形式にする事が可能である。 \nocite{*}