• プログラムの信頼性を保証する方法の１つとしてモデル検査がある。 モデル検査を行う場合はプログラムの持ち得る全ての状態を調べる、SPINまたはjava path finderを用いて行われる。しかし、SPINで行う場合にはPROMELAに書き換える必要がありjava path finder はjavaのバイトコードを検証するためのものであるが、大きなプログラムの検証や複数プロセスが扱えないなどの問題点がある。 本研究ではGeasOS上でDPPのモデルチェッキングを行ことで、書き換えを必要とせず、複数プロセスのプログラムの検証を行う

# 課題

• GeasOSはgotoによる遷移を行うため、stackを積まない。
• しかし、モデル検査はDepth firstで行われるため、1つ前の状態に戻る必要がある。そこでモデル検査をおこなうために、、、
• iterator を使ってのマルチスレッドモデル検査を実装する。