view paper/text/Jabstract.tex @ 30:73db994b71f4

...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Fri, 28 Jan 2022 02:43:51 +0900
parents 737734bb3877
children
line wrap: on
line source

アプリケーションの信頼性を保証することは
情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である.
アプリケーションの信頼性を保証するために,基盤となるOSの信頼性を高める必要がある.
信頼性を保証するための手法として定理証明やモデル検査が挙げられる.

当研究室では,定理証明やモデル検査による信頼性の保証を目的としたGearsOSを開発している.
GearsOSはノーマルレベル,メタレベルの処理を切り分けることができる
Continuation Based C(CbC)で記述されており,Gearというプログラミング概念を持つ.
CbCでメタレベルの処理を切り出したものに対して定理証明やモデル検査を行うことで
信頼性を保証する\cite{modelcheck}.

GearsOSには現在未実装の機能があり,その一つにファイルシステムが挙げられる.
Unixのファイルシステムではファイルのメタデータをinodeの形式で保持している.
同様にinodeの仕組みを用いてGearsOSのファイルシステムを実装したい.
また,当研究室で開発している分散フレームワークChristieの仕組みを用いて,分散ファイルシステムを実装したい.

本論文では,まずGearsOSのファイルシステム構築に関する基礎概念の紹介をし,
その後GearsOSのファイルシステムの具体的な構築方法について述べる.