2006 Fiscal Year Annual Research Report
| Project/Area Number |
18500043
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Keywords | 設計検証 / モデル検査 / 遷移関係 / モジュール分割 / 共有二分決定グラフ / 並列アルゴリズム |
|---|
| Research Abstract |
1.モジュールの依存関係に基づく遷移関係の分割とモデル検査
モジュール間の依存関係として、依存度の強いモジュール同士をグループ化することによりシステム全体の遷移関係をバランス良く分割するアルゴリズムの検討を行った。まず、モジュールの依存関係をベースにした構造分割を行い、構造分割により得られたモジュールのグループに対するモデル検査を組み合わせることによりシステム全体のモデル検査を行う合成的モデル検査法を可能とするための十分条件を示した。次に、各グループのモデル検査に対して、変数の依存関係に基づいて場合分けする分割手法を構築した。さらに、分割された各場合に対して、対象性を考慮した抽象化の検討を行った。これらの手法の組合せにより、モデル検査の効率を大幅に向上できるものと期待される。
2.関数ベクトル方式による状態集合処理
特徴関数による状態集合の表現法では、特徴関数を表すBDDの節点数爆発がボトルネックになることが多い。そこで、状態集合の表現として関数ベクトルを用い、それを利用した集合演算や像計算を実現するアルゴリズムの検討を開始した。
3.像計算の並列アルゴリズム
論理関数のコファクタ分解による並列BDD処理アルゴリズムをベースにして、遷移関係の分割等も利用し、種々の並列アーキテクチャに対応した並列像計算アルゴリズムを検討した。これらのアルゴリズムでは、クラスタシステムにおけるノード間BDD転送の減少を目標とし、また、共有メモリ型並列計算機における共有変数のロック回数を減らすことを考慮している。現在これらのアルゴリズムのプロトタイプを試作中であり、今後これらのアルゴリズムの評価を行う予定である。
|
