2007 Fiscal Year Annual Research Report
| Project/Area Number |
18500043
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 Kyoto Sangyo University, 工学部, 教授 (40093299)
|
|---|
| Keywords | 設計検証 / モデル検査 / 遷移関係 / モジュール分割 / 共有二分決定グラフ / 並列アルゴリズム |
|---|
| Research Abstract |
1.モジュールの依存関係に基づく遷移関係の分割とモデル検査:モジュールの依存関係をベースにした構造分割を用いる合成的モデル検査法の評価を進めた。とくに、構造分割により得られるモジュールのグループに対して、対称性や帰納的性質を考慮した抽象化を行うために、ケース分割手法を取り入れ、そのために必要な変数の選び方として、変数間の依存関係を考慮した選び方などについて検討した。また、分割サイズ等のパラメータを問題に応じて動的に調整するアルゴリズムの研究も開始した。
2.関数ベクトル方式による状態集合処理とモデル検査:関数ベクトルを用いた状態集合の表現と、それを利用した集合演算や像計算を実現するアルゴリズムの研究を進めた。関数ベクトル方式に対しても、モジュールの依存関係に基づいて関数ベクトルを分割することにより効率向上が期待できることが判明し、分割された関数ベクトルによる集合演算や像計算アルゴリズムの研究を開始した。分割された関数ベクトルどうしが互いに同型である場合や対象性を有する場合も考えられ、このような場合に適用可能な抽象化手法についても検討を行った。
3.モデル検査の並列アルゴリズム:像計算の並列アルゴリズムを、モジュールの依存関係に基づく遷移関係や関数ベクトルの分割を利用した並列像計算アルゴリズムと比較検討し、クラスタ・システムや共有メモリ型並列計算機、ハイパー・スレッディングやマルチ・コア技術による安価な並列計算機に適したモデル検査アルゴリズムの検討を行った。また、モデル検査を充足可能性判定問題(SAT)に帰着する方法を明らかにした。今後SATの並列アルゴリズムについても検討し、これまでに判明しているアルゴリズムとの比較を進める予定である。
|
