changeset 20:737734bb3877

...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Wed, 26 Jan 2022 18:53:42 +0900
parents 9d7c2f216e62
children 14faefbdd1b5
files paper/text/Eabstract.tex paper/text/Jabstract.tex paper/thesis.pdf paper/thesis.tex
diffstat 4 files changed, 8 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/paper/text/Eabstract.tex	Wed Jan 26 14:58:06 2022 +0900
+++ b/paper/text/Eabstract.tex	Wed Jan 26 18:53:42 2022 +0900
@@ -1,7 +1,7 @@
-Ensuring the reliability of applications is an important issue for ensuring the reliability of information systems and operations that use computers. In order to guarantee the reliability of applications, it is necessary to improve the reliability of the underlying operating system. Theorem proving and model checking are the methods to guarantee the reliability.
+Ensuring the reliability of applications is an To guarantee the reliability of applications, it is necessary to improve the reliability of the underlying operating system. In order to guarantee the reliability of applications, it is necessary to improve the reliability of the underlying operating system. Theorem proving and model checking are the methods to guarantee the reliability.
 
-In our laboratory, we are developing GearsOS for the purpose of guaranteeing reliability by theorem proving and model checking. GearsOS is written in Continuation Based C (CbC), which can separate normal-level and meta-level processing, and has the programming concept of Gear. GearsOS is written in Continuation Based C (CbC), which can separate normal-level and meta-level processing.
+In our laboratory, we are developing GearsOS to guarantee the reliability by theorem proving and model checking. GearsOS is capable of separating normal-level and meta-level processing. GearsOS is written in Continuation Based C (CbC) and has a programming concept called Gear. By performing theorem proving and model checking on the meta-level processing extracted by CbC\cite{modelcheck}.
 
-There are currently unimplemented features in GearsOS, one of which is the file system. We would like to implement a file system for GearsOS that can guarantee reliability through model checking.
+There are currently unimplemented features in GearsOS, one of which is the file system. The Unix file system stores file metadata in the form of inodes. We would like to implement a file system for GearsOS using the same inode mechanism.
 
-In this paper, we first introduce the basic concept of the file system construction of GearsOS, and then describe the concrete construction method of the file system of GearsOS.
\ No newline at end of file
+In this paper, we first introduce the basic concept of the GearsOS file system construction. This paper first introduces the basic concept of the file system construction of GearsOS, and then describes the concrete construction method of the file system of GearsOS.
\ No newline at end of file
--- a/paper/text/Jabstract.tex	Wed Jan 26 14:58:06 2022 +0900
+++ b/paper/text/Jabstract.tex	Wed Jan 26 18:53:42 2022 +0900
@@ -10,7 +10,8 @@
 信頼性を保証する\cite{modelcheck}.
 
 GearsOSには現在未実装の機能があり,その一つにファイルシステムが挙げられる.
-信頼性をモデル検査を通して保証することができるGearsOSのファイルシステムを実装したい.
+Unixのファイルシステムではファイルのメタデータをinodeの形式で保持している.
+同様にinodeの仕組みを用いてGearsOSのファイルシステムを実装したい.
 
 本論文では,まずGearsOSのファイルシステム構築に関する基礎概念の紹介をし,
 その後GearsOSのファイルシステムの具体的な構築方法について述べる.
\ No newline at end of file
Binary file paper/thesis.pdf has changed
--- a/paper/thesis.tex	Wed Jan 26 14:58:06 2022 +0900
+++ b/paper/thesis.tex	Wed Jan 26 18:53:42 2022 +0900
@@ -2,8 +2,8 @@
 \usepackage{ie-thesis}
 \usepackage{listings}
 
-\jtitle{GearsOSにおけるinodeを用いたFileSystemの設計}
-\title{Designing a FileSystem in GearsOS}
+\jtitle{GearsOSにおけるinodeを用いたFile systemの設計}
+\title{Design of a File system using inodes in GearsOS}
 
 \affiliation{琉球大学工学部工学科知能情報コース}
 \studentid{185742J}