|
37
|
1 # 研究目的
|
|
|
2 - アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
|
|
|
3 - しかしOSの機能をテストですべて検証するのは不可能である。
|
|
|
4 - 定理証明やモデル検査を利用して、テストに頼らずに保証したい
|
|
|
5 - 証明しやすい形、かつ実際に動くソースコードが必要
|
|
|
6 - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
|
|
|
7 - プログラムは二つの計算に分離される
|
|
|
8 - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
|
|
|
9 - その計算に必要なメタな計算(メタレベル)
|
|
|
10 - プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
|
|
|
11 - そのためにはメタレベルの計算を柔軟に扱うAPIや, メタレベルを保証しつつCbCを拡張した実装方法が必要
|
|
|
12 - 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ>計算APIについて考察する。
|
|
|
13
|
|
|
14
|
|
|
15
|
|
|
16 # 今週
|
|
|
17 - windowsにした
|
|
|
18 - linuxにしたい
|
|
|
19 - 修論かいてる
|
|
|
20 - がんばろう
|
