既存のモデル検査ツールSPINは並行プログラムのデバッグにおいて有用であるがシミュレーション実行によるデバッグを合わせて行うことも大きな効果が見込まれる。
ランダムシミュレーションでは、ランダムに得られた動作列に着目するため開発者が想定していない箇所での仕様の漏れやバグを発見できるメリットがある。
このとき動作列の全状態中の位置を可視化できればデバッグに有用であると考えられる。
そこで本研究ではシミュレーション結果から抽出した状態遷移図とJSPINから静的に得られる状態遷移図をマージした状態遷移図を出力するツールを設計した。
本発表では本ツールの設計およびプロトタイプ実装について述べ有効性を考察する。