changeset 5:13a699ab5cee

first chapter modify
author e165723 <e165723@ie.u-ryukyu.ac.jp>
date Tue, 07 May 2019 21:16:04 +0900
parents f028af8ad951
children 8dd84d4179f8
files Paper/sigos.pdf Paper/sigos.tex
diffstat 2 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
Binary file Paper/sigos.pdf has changed
--- a/Paper/sigos.tex	Tue May 07 21:12:29 2019 +0900
+++ b/Paper/sigos.tex	Tue May 07 21:16:04 2019 +0900
@@ -58,7 +58,7 @@
 
 \maketitle
 
-\section{OS }
+\section{OS の評価の容易化}
 OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。現段階で動作する OS として xv6 を採用し、 CbCで書き換えることにより stackを排除し状態遷移化することができる。状態遷移化することにより状態を有限化させることが可能となるため、評価が容易になる。よって評価を容易にするためにxv6 kernel をCbC で書き換え状態遷移に落とし込むことを目的とする。