• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2001 年度 実績報告書

ワークステーションクラスタによる並列分散型形式的論理設計検証

研究課題

研究課題/領域番号 12680361
研究機関京都産業大学

研究代表者

平石 裕実  京都産業大学, 先端科学技術研究所, 教授 (40093299)

キーワード設計検証 / 論理設計 / 形式的検証 / 並列処理 / 分散処理 / クラスタシステム
研究概要

本年度は、VIAに基づく超高速スイッチで結合された約100台の専用PCクラスタを用いて、クラスタシステムの基本性能評価、二分決定図の並列アルゴリズム、並列プログラムの検証等の研究を行い、以下のような成果を得た。
1.VIAに基づく専用PCクラスタの評価:
種々のレベルでの並列分散検証アルゴリズムで必要となる各種のデータ転送パタンに対してVIAに基づく専用PCクラスタにおける転送速度等の基本性能評価を行った。基本的な送受信で50-90MB/sec、分配収集で1段辺り75-100MB/secの転送速度を実現出来た。
2.共有二分決定図の並列分散処理アルゴリズムの構築:
まず、共有二分決定図(BDD)のこのコファクタ分解をベースにして、基本論理演算の並列アルゴリズムを構築し、性能評価を行った結果、並列度の0.3-0.5倍程度の加速率を達成でき、また、BDDの総節点数の増加が2.5-3.5倍程度になることが判明した。また、設計検証で重要なスムージング演算、サポート演算、代入演算、像計算、逆像計算等の並列アルゴリズムを検討し、BDDのストリーミング送受信に基づく並列アルゴリズムを提案した。今後、性能評価のためのプログラム開発を行う予定である。
3.並列分散プログラムの検証:
メッセージパッシング方式の並列分散プログラムの設計検証に関して、デッドロックが無いことを検証するための数学モデルを種々検討した。この問題は、一般的にプログラムの停止性判定問題を含むため決定不能であるが、プログラムの形に制限を加えることによりfalse negativeな検証は可能になる可能性があり、どのような制限を加えればよいかについて検討していく予定である。

  • 研究成果

    (1件)

すべて その他

すべて 文献書誌 (1件)

  • [文献書誌] Hiromi Hiraishi: "Verification of Deadlock Free Property of Asynchronous Robot Control Programs"京都産業大学先端科学技術研究所所報. 1. (2002)

URL: 

公開日: 2003-04-03   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi