モデル検査ツールSPINによる並行プログラムのデバッグを支援する状態遷移追跡支援ツールの設計と実装

情報処理学会

この論文をさがす

抄録

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

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ