changeset 4:1a881e24e438

tweak
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 21 Nov 2019 12:51:22 +0900
parents 450d0e91835b
children d31ae35efec0
files paper/anatofuz_prosym_2019.pdf paper/anatofuz_prosym_2019.tex
diffstat 2 files changed, 4 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
Binary file paper/anatofuz_prosym_2019.pdf has changed
--- 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{*}