/ プログラム/ 発表一覧/ 著者一覧/ 企業展示一覧/ jsai2010ホーム /

2E1-3 強連結成分の性質を用いたOWCTYモデル検査アルゴリズムの高速化

06月10日(Thu) 09:00〜10:00 E会場(3F-会議室5)
2E1 基礎・理論「探索・プランニング」

演題番号2E1-3
題目強連結成分の性質を用いたOWCTYモデル検査アルゴリズムの高速化
著者川端 聡基(早稲田大学理工学部コンピュータ・ネットワーク工学科)
小林 史佳(早稲田大学理工学研究科情報・ネットワーク専攻)
上田 和紀(早稲田大学理工学術院情報理工学科)
時間06月10日(Thu) 09:40〜10:00
概要モデル検査はグラフの網羅的探索を行う検証手法であり,高速化が求められている. 並列モデル検査手法であるOWCTYはエラーのないモデルで高速に動作する手法であるが,扱うグラフの特性を利用し切っているとは言えず高速化の余地がある.そこで,我々は強連結成分を利用した改良手法としてSCC-OWCTYを提案する.分散検証環境DiVinEを用いて既存の手法との比較を行い,SCC-OWCTYの有効性を検討する.
論文PDFファイル