--- a/paper/chapter/abstract.tex	Fri Feb 05 09:53:09 2021 +0900
+++ b/paper/chapter/abstract.tex	Fri Feb 05 10:24:40 2021 +0900
@@ -27,4 +27,23 @@
 本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察し、言語機能などの拡張を行った。
 また、メタ計算を自動生成しているトランスコンパイラを改良し、従来のGearsOSのシステムよりさらに柔軟性が高いものを考案した。
 \chapter*{Abstract}
-hogefuga
+In order to guarantee the reliability of an application, the reliability of the underlying OS must be highly guaranteed.
+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.
+It is impossible to verify all the functions of an OS by testing.
+
+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.
+For theorem proving to guarantee reliability using proofs, we can use theorem proving support systems such as Agda and Coq.
+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.
+
+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.
+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.
+
+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.
+A language that can describe both levels is Continuation Based C (CbC).
+CbC is characterized by the fact that it does not have a stack or an environment, and the next process is performed by continuation.
+Using CbC, we are developing GearsOS, an OS that is both scalable and reliable.
+
+The development of GearsOS requires both normal-level code and meta-level code, and the number of meta-level computations varies widely.
+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.
+In this study, we discussed the API for meta-calculus, which will guarantee the reliability and scalability of GearsOS, and extended the language functions.
+We also improved the trans-compiler that automatically generates meta-calculus, and devised a system that is more flexible than the conventional GearsOS system.

Binary file paper/master_paper.pdf has changed