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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12680361
• Research Institution: Kyoto Sangyo University
• Principal Investigator: 平石 裕実 京都産業大学, 工学部, 教授 (40093299)
• Keywords: 設計検証 / 論理設計 / 形式的検証 / 並列処理 / 分散処理 / クラスタシステム

Research Abstract

本年度は、2種類のPCワークステーションクラスタシステムを構築し、その基本性能評価を行うとともに、クラスタシステム上での実行に適した検証アルゴリズムに関して基礎的な考察を行い、以下の成果を得た。
1.本学の情報処理教室に設置されている約700台のPC上に並列処理用ライブラリとしてPVMとMPIをインストールしてクラスタシステムを構築し、並列処理用ライブラリの元でのデータ転送速度等の基本性能評価を行った。このシステムで用いているPCは昼間は授業等で利用されているためクラスタシステムとして利用できるのは夜間と祝日のみである。そこで、別途60台のPCを用いて並列検証プログラムの開発等に常時利用可能なクラスタシステムも構築した。後者のクラスタシステムは、Gbpsの速度の超高速ネットワークを用いてVIAで接続を行った。これによりMPIによるデータ転送で60-100Mバイト/秒の転送速度を実現した。また、これらのクラスタシステムの状態を把握するため、CPU利用率、ネットワーク使用状況等をリアルタイムで表示する状態表示プログラムを開発した。
2.クラスタシステム上での実現に適した検証アルゴリズムに関して、基礎的な考察を行った。具体的に、多数のプロセスで構成されるロボット制御システムのデッドロックフリー性の検証問題を取り上げ、まず、直列検証アルゴリズムの改良を行い、千倍以上の高速化を達成した。次に、この直列検証アルゴリズムに対して、仕様レベル、記号モデル検査レベル、BDD演算レベル、BDD演算のための変数の順序付けレベルでの並列化の検討を開始した。

Research Products

• [Publications] Hiromi Hiraishi: "Yet More Image Computations for SMV, the Symbolic Model Verifier"Systems and Computers in Japan. 31・9. 1-9 (2000)
• [Publications] Hiromi Hiraishi: "Verification of Deadlock Free Property of High Level Robot Control"Proceedings of the 9th Asian Test Symposium. 9. 198-203 (2000)