--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/Moririn/メモ/2023/04/24.md	Tue Apr 25 00:10:03 2023 +0900
@@ -0,0 +1,15 @@
+# 研究目的
+
+
+- メモ書き  
+OSの信頼性は高ければ高いほど良い --  
+当研究室ではGearsOSというOSを開発している。  
+GearsOSの信頼性を高めたい。  
+このGearsOSにRedBlackTreeの概念を使用したい。
+RedBlackTreeが正しくGearsOS上で動作するかを検証する必要がある。  
+この検証手法としてAgdaを使用する。    
+GearsOSとは、CbCという言語で書かれている。  
+Cbcの概念を取り入れたGearsAgdaでRedBlackTreeを実装していく  
+RedBlackTreeとは、２分木の一種で、赤と黒の色の概念がある。どのノードを見ても黒色の深さが一定である。木が崩れた場合はバランスするという特徴がある。  
+BinaryTreeはできているので、これを利用してRedBlackTreeを書いていく。  
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/harutori.md	Tue Apr 25 00:10:03 2023 +0900
@@ -0,0 +1,2 @@
+# harutori
+This is harutori's page
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/2023/research_plan.md	Tue Apr 25 00:10:03 2023 +0900
@@ -0,0 +1,28 @@
+# 令和5年度研究計画書
+
+## 研究題目
+
+Gears OSのファイルシステムとDB
+
+## 研究目的
+
+当研究室では，Continuation based C（CbC）を用い，定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している．OSにおいてFSは重要な機能の一つであるため実装する必要がある．その際，証明や検証を容易に行えるようになるべくシンプルな実装を考えたい．
+
+## 研究内容
+
+証明や検証を容易に行うため，FSとDBの実装をすべてRedBlackTreeで行う．FSとDBは本質的に同じものであるが，スキーマの有無などの違いがあるため，違いの部分を考察しつつ同一のRedBlackTreeで実装する．(FSとして実装したものがそのままDBとなりうると考える．) また，信頼性の向上のためトランザクションとロールバック，バックアップなどをRedBlackTreeに適した形で実装し，それぞれ検証する．全体としては，証明や検証への適正，システムとしての信頼性の確認，RedBlackTreeのみでの実装に関する考察を行う．
+
+## 研究計画
+
+~ 5月15日 OS研究会準備(実装・スライド・発表練習)
+
+5月16日 ~ 5月17日 OS研究会発表
+
+5月17日 ~ 11月 実装と検証
+- 特にトランザクション部分やロールバック，バックアップ部分などシステムの信頼性に関わる部分の検証を行う
+
+2024年
+
+1月 修論提出
+
+2月 修論発表
\ No newline at end of file