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