|
2
|
1 # Gears OSのモデル検査を用いた設計
|
|
|
2
|
|
|
3 # 研究目的
|
|
|
4 プログラムの信頼性を保証するには、プログラムの証明、またはモデル検査がある。
|
|
|
5 モデル検査を行う場合はプログラムの持ち得る全ての状態を調べる事になり、SPINかjava path finderが一般的には用いられるが、SPINで行う場合にはPROMELAに書き換える必要がありjava path finder はjavaのバイトコードを検証するためのものであるが、大きなプログラムの検証や複数プロセスが扱えないなどの問題点がある。
|
|
|
6 本研究ではGeasOS上でDPPのモデルチェッキングを行ことで、書き換えを必要とせず、複数プロセスのプログラムの検証を行う
|
|
|
7
|
|
|
8
|
|
|
9
|
|
0
|
10
|
|
|
11 # 要約
|
|
|
12 * CbC は処理の移行を goto 用いて行い、データ構造はdate gearにより保持する事でプログラムの処理をcode gear毎の独立したものにする。
|
|
|
13 * Geas OS はCbCで記述されおり、処理を変更する事なく処理の間に自由にメタ処理を挟む事ができる、これにスケジューラーを挟む事でマルチスレッド処理などが可能となる。
|
|
2
|
14 * メタ計算部分にモデルチェッキングを入れる事でプログラムを実行しながらにして証明することが可能となる。
|
|
|
15 * モデルチェッキングはdepth firstで行われる、しかしGeasOSはstackがないため、ポインタを使って戻ることができない、そこで |
