Mercurial > hg > Papers > 2020 > anatofuz-sigos
changeset 8:92988591be65
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 Apr 2020 13:16:59 +0900 |
| parents | 8f1d03a81516 |
| children | 880da2d67bab |
| files | paper/Makefile paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf |
| diffstat | 3 files changed, 4 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/Makefile Thu Apr 30 13:10:39 2020 +0900 +++ b/paper/Makefile Thu Apr 30 13:16:59 2020 +0900 @@ -14,7 +14,7 @@ .SUFFIXES: .md .tex .dvi .pdf .md.tex: - perl md2tex.pl $(TARGET).md > $(TARGET).tex + perl md2tex.pl $< > $@ .tex.dvi: $(LATEX) $< @@ -34,7 +34,7 @@ pdf: $(TARGET).pdf vi: - vim $(TARGET).tex + vim $(TARGET).md clean:
--- a/paper/anatofuz-sigos.md Thu Apr 30 13:10:39 2020 +0900 +++ b/paper/anatofuz-sigos.md Thu Apr 30 13:16:59 2020 +0900 @@ -12,10 +12,11 @@ これに適した形として、 状態遷移モデルが挙げられる。 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。 -分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語で再実装することで仕様の整合性を検証する事が可能である。 +分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語を用いて再実装することで仕様の整合性を検証する事が可能である。 しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。 現在小さなunixであるxv6 kernelを状態遷移を基本とした単位でのプログラミングに適した言語、 Continuation Based Cを用いて再実装している。 再実装の為には、 既存のxv6 kernelの処理の状態遷移を、継続を用いたプログラムに変換していく必要がある。 +