Mercurial > hg > Papers > 2021 > anatofuz-master

comparison paper/chapter/introduction.tex @ 23:c69811b44e7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Sat, 30 Jan 2021 16:22:52 +0900
parents 36d241194507
children 9c443292fbfb
comparison
equal deleted inserted replaced
22:ada9b562891d 23:c69811b44e7c
1 \chapter{継続を中心としたプログラミングスタイル} 1 \chapter{OSとアプリケーションの信頼性}
2 2
3 コンピューター上では様々なアプリケーションが常時動作している。 3 コンピューター上では様々なアプリケーションが常時動作している。
4 動作しているアプリケーションは信頼性が保証されていてほしい。 4 動作しているアプリケーションは信頼性が保証されていてほしい。
5 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。 5 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
6 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。 6 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。
32 検証ができているソースコードそのものを使ってOSを動作させたい。 32 検証ができているソースコードそのものを使ってOSを動作させたい。
33 33
34 34
35 他の形式手法にモデル検査がある。 35 他の形式手法にモデル検査がある。
36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
37 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
37 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 38 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
38 実装するコードに対してモデル検査を行いたいが、モデル検査を行うモデル検査器は限られている。 39 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
39 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 40 しかしOSの処理は膨大であり、 様々な関数呼び出しや非決定的な処理、 並行処理などが発生する。
41 モデル検査を行う場合でも、やみくもにOSのすべての処理を検査するのは難しい。
42
43
44 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
45 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
46 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
47 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
48 この為にはOSの処理を状態遷移系で表現し、 証明しやすくする必要がある。
49
50
51 OSを状態遷移系で実装する場合、通常のC言語では状態ごとに分離するのは困難である。
52 関数呼び出しを利用して状態を切り分けても、 関数呼び出し時に伴うスタックフレームの操作などでパフォーマンスにも問題がある。
53 この問題を解決するには、 C言語よりも細かく記述できる言語で実装する必要がある。