|
2
|
1 \chapter*{要旨}
|
|
55
|
2 アプリケーションの信頼性を保証するには、土台となるOSの信頼性は高く保証されていなければならない。
|
|
|
3 信頼性を保証する方法としてテストコードを使う手法が広く使われている。
|
|
|
4 OSのソースコードは巨大であり、並列処理など実際に動かさないと発見できないバグが存在する。
|
|
|
5 OSの機能をテストですべて検証するのは不可能である。
|
|
|
6
|
|
|
7 テストに頼らず定理証明やモデル検査などの形式手法を使用して、OSの信頼性を保証したい。
|
|
|
8 証明を利用して信頼性を保証する定理証明は、 AgdaやCoqなどの定理証明支援系を利用することになる。
|
|
|
9 支援系を利用する場合、各支援系でOSを実装しなければならない。
|
|
|
10 証明そのものは可能であるが、 支援系で証明されたソースコードがそのままOSとして動作する訳ではない。
|
|
|
11 このためには定理証明されたコードを等価なC言語などに変換する処理系が必要となる。
|
|
|
12
|
|
|
13 信頼性を保証するほかの方法として、プログラムの可能な実行をすべて数え上げて仕様を満たしているかを確認するモデル検査がある。
|
|
|
14 モデル検査は実際に動作しているプログラムに対して実行することが可能である。
|
|
75
|
15 すでに実装したプログラムのコードに変化を加えずモデル検査を行いたい。
|
|
55
|
16
|
|
75
|
17 プログラムは本来やりたい計算であるノーマルレベルの計算と、その計算をするのに必要なメタレベルの計算に別けられる。
|
|
|
18 メタレベルの計算では資源管理などを行うが、 モデル検査などの証明をメタレベルの計算で行いたい。
|
|
2
|
19
|
|
75
|
20 この実現にはノーマルレベル、メタレベルの計算の処理の切り分けと、メタレベルの計算をより柔軟に扱うOS、言語処理系が必要となる。
|
|
|
21 両レベルを記述できる言語にContinuation Based (CbC)がある。
|
|
|
22 CbCはスタック、あるいは環境を持たず継続によって次の処理を行う特徴がある。
|
|
|
23 CbCを用いて、拡張性と信頼性を両立するOSであるGearsOSを開発している。
|
|
|
24
|
|
|
25 GearsOSの開発ではノーマルレベルのコードとメタレベルのコードの両方が必要であり、メタレベルの計算の数は多岐にわたる。
|
|
|
26 GearsOSの開発を進めていくには、メタレベルの計算を柔軟に扱うAPIや、 自動でメタレベルの計算を作製するGearsOSのビルドシステムが必須となる。
|
|
|
27 本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察し、言語機能などの拡張を行った。
|
|
91
|
28 また、メタ計算を自動生成しているトランスパイラを改良し、従来のGearsOSのシステムよりさらに柔軟性が高いものを考案した。
|
|
2
|
29 \chapter*{Abstract}
|
|
83
|
30 In order to guarantee the reliability of an application, the reliability of the underlying OS must be highly guaranteed.
|
|
|
31 The source code of an OS is huge, and there are bugs such as parallel processing that can only be discovered by actually running the OS.
|
|
|
32 It is impossible to verify all the functions of an OS by testing.
|
|
|
33
|
|
|
34 Instead of relying on tests, we want to use formal methods such as theorem proving and model checking to guarantee the reliability of the OS.
|
|
|
35 For theorem proving to guarantee reliability using proofs, we can use theorem proving support systems such as Agda and Coq.
|
|
|
36 Another method of guaranteeing reliability is model checking, in which all possible executions of a program are counted to verify that it meets the specifications.
|
|
|
37
|
|
|
38 A program can be divided into normal-level computation, which is the computation we want to do, and meta-level computation, which is the computation necessary to do the computation.
|
|
|
39 In meta-level computation, we want to perform resource management, etc., but we also want to perform proofs such as model checking in meta-level computation.
|
|
|
40
|
|
|
41 In order to achieve this, it is necessary to separate the processing of normal-level and meta-level computation, and to have an OS and language processing system that can handle meta-level computation more flexibly.
|
|
|
42 A language that can describe both levels is Continuation Based C (CbC).
|
|
|
43 CbC is characterized by the fact that it does not have a stack or an environment, and the next process is performed by continuation.
|
|
|
44 Using CbC, we are developing GearsOS, an OS that is both scalable and reliable.
|
|
|
45
|
|
|
46 The development of GearsOS requires both normal-level code and meta-level code, and the number of meta-level computations varies widely.
|
|
|
47 In order to proceed with the development of GearsOS, an API that can flexibly handle meta-level computations and a build system for GearsOS that can automatically create meta-level computations are essential.
|
|
|
48 In this study, we discussed the API for meta-calculus, which will guarantee the reliability and scalability of GearsOS, and extended the language functions.
|
|
|
49 We also improved the trans-compiler that automatically generates meta-calculus, and devised a system that is more flexible than the conventional GearsOS system.
|
