# HG changeset patch # User e165723 # Date 1557231364 -32400 # Node ID 13a699ab5cee25ddd82182933b50b352fad86c76 # Parent f028af8ad9513d4dbaf658c201c0fb43c9eeca2b first chapter modify diff -r f028af8ad951 -r 13a699ab5cee Paper/sigos.pdf Binary file Paper/sigos.pdf has changed diff -r f028af8ad951 -r 13a699ab5cee Paper/sigos.tex --- 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 で書き換え状態遷移に落とし込むことを目的とする。