Mercurial > hg > Papers > 2020 > anatofuz-sigos

Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Thu Apr 30 13:16:59 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-%%
-%% 研究報告用スイッチ
-%% [techrep]
-%%
-%% 欧文表記無しのスイッチ(etitle,eabstractは任意)
-%% [noauthor]
-%%
-
-%\documentclass[submit,techrep]{ipsj}
-\documentclass[submit,techrep,noauthor]{ipsj}
-
-
-
-\usepackage[dvips]{graphicx}
-\usepackage{latexsym}
-
-\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
-\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
-\def\|{\verb|}
-%
-
-%\setcounter{巻数}{59}%vol59=2018
-%\setcounter{号数}{10}
-%\setcounter{page}{1}
-
-
-\begin{document}
-
-
-\title{xv6の構成要素の継続の分析}
-
-%\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}
-
-\affiliate{KIE}{琉球大学大学院理工学研究科情報工学専攻}
-\affiliate{IE}{琉球大学工学部工学科知能情報コース}
-
-
-\author{清水 隆博}{Shimizu Takahiro}{KIE}[anatofuz@cr.ie.u-ryukyu.ac.jp]
-\author{河野 真治}{Shinji Kono}{IE}
-
-\begin{abstract}
-OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
-テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。
-
-状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
-このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
-本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
-\end{abstract}
-
-
-\maketitle
-
-\section{OSの信頼性}
-様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
-アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
-OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
-しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
-また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
-テスト以外の方法でOSの信頼性を高めたい。
-
-数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
-OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
-これらで信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
-
-
-\nocite{*}
-\bibliographystyle{ipsjunsrt}
-\bibliography{anatofuz-bib}
-
-
-
-\end{document}