2008 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.検証対象の簡略化と抽象化アルゴリズム:モジュールの依存関係を利用したモデル検査の効率化手法を合成モデル検査法と組み合わせることにより、検証対象を抽象化する方法を検討した。検証する性質や仕様ごとに検証のための内部モデルを再構築する方法の場合、検証項目と独立した部分を簡略化することが可能であり、検証対象の簡略化と抽象化アルゴリズムの研究を進めた。
|
