Mercurial > hg > Document > Growi

changeset 128:8dfc12dd7740

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
backup 2023-06-13
author autobackup
date Tue, 13 Jun 2023 00:10:03 +0900
parents 252d26ac7623
children 4bbd08ccb3c2
files user/Moririn/メモ/2023/04/24.md user/Yoshisuar.md user/matac42/notes/__template.md
diffstat 3 files changed, 42 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/user/Moririn/メモ/2023/04/24.md	Tue Jun 06 00:10:03 2023 +0900
+++ b/user/Moririn/メモ/2023/04/24.md	Tue Jun 13 00:10:03 2023 +0900
@@ -2,10 +2,7 @@
 
 OSを含むアプリケーションは、高い信頼性を持つことが望ましい。
 当研究室では、CbC(Continuation based C)を採用した GearsOS を開発しており、信頼性を高めることが現在
-の課題である。信頼性を高める手法として、テストやモデル検査などが考えられるが、数学的な証
-明を行うことでも信頼性を上げることができる。ここでは、GearsAgda を用いた検証を行うこと
-で、信頼性の向上を図る。GearsAgda とは、CbC を定理証明支援系言語 Agda で記述する手法で
-あり、GearsOS の検証において最適である。     
+の課題である。信頼性を高める手法として、テストやモデル検査などが考えられるが、数学的な証明を行うことでも信頼性を上げることができる。ここでは、GearsAgda を用いた検証を行うことで、信頼性の向上を図る。GearsAgda とは、CbC を定理証明支援系言語 Agda で記述する手法であり、GearsOS の検証において最適である。     
    本研究は、GearsOS に採用する二分探索木 RedBlackTree を GearsAgda で検証し実装するこ
 とで OS の信頼性を向上させることが目的である。RedBlackTree とは、バランスした二分探索木
 の一種であり、バランスを保つために木が回転することや、根から任意の葉ノードまでのパス上の
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/Yoshisuar.md	Tue Jun 13 00:10:03 2023 +0900
@@ -0,0 +1,2 @@
+# Yoshisuar
+This is Yoshisuar's page
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/notes/__template.md	Tue Jun 13 00:10:03 2023 +0900
@@ -0,0 +1,39 @@
+# 研究目的
+
+## システム全体の信頼性を上げたい
+
+- システムの構成要素全体の信頼性を上げる必要がある
+  - アプリケーション
+  - OS
+  - ファイルシステム
+  - DB
+  - メモリとSSD
+  - 分散ノード
+  - ネットワーク
+
+---
+
+## Gears OSを使って実現する
+
+- CodeGear
+  - 処理の単位
+- DataGear
+  - データの単位
+- metaGear
+  - データの整合性
+  - 資源管理
+
+---
+
+## 信頼性を上げる方法
+
+- 証明
+  - GearsAgdaを使ってinvariantを証明する
+- テスト
+- モデル検査
+- システムの構成要素全体にこれらの方法を適用したい
+- 既存システムの信頼性における問題点の解決
+
+---
+
+## 進捗など