| 研究課題/領域番号 |
09680348
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 京都産業大学 |
|---|
研究代表者 |
平石 裕実 (平石 裕美) 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| 研究期間 (年度) |
1997 – 1998
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
3,700千円 (直接経費: 3,700千円)
1998年度: 1,500千円 (直接経費: 1,500千円)
1997年度: 2,200千円 (直接経費: 2,200千円)
|
|---|
| キーワード | 設計検証 / 論理設計 / 形式的検証 / 時相論理 / 記号モデル検査 / 分散アルゴリズム / BDD / 論理設計検証 / 様相論理 / 並列アルゴリズム |
|---|
| 研究概要 |
形式的論理設計検証に関して以下の研究成果を得た。
1. 拡張時空間様相論理: 時空間様相論理で有限長ビットスライス回路を取り扱うために必要な拡張を行った。本拡張では、仮想的にビット位置カウンタを設置し、指定位置で出力を無効化する信号を生成する。この信号を用いて、指定位置以降の出力を無視することにより、有限長ビットスライス回路のモデル化を行った。
2. 並行プロセスの検証: 多数の並行プロセスとしてシステム全体をモデル化した場合に適した検証アルゴリズムを考案した。本手法では、プロセス変数や値の変化しない状態変数を(逆)像計算に先立ちスムージングや代入操作を行っている。これにより、記号モデル検査を10倍以上高速化出来ることを示した。
3. 並列分散プロセス順序付けアルゴリズム: BDDの変数順序づけとして、プロセス単位でグループ化して順序づけを行う手法を提案した。順序づけには、評価値を分枝限定法により最適化する並列分散アルゴリズムを示した。実際に25台の計算機で実行した結果、スーパーリニア効果が得られることが判明した。
4. タスク制御アーキテクチャの検証: 多数の並行プロセスとしてモデル化できるシステムの例として、ロボット制御プログラムのタスク制御アーキテクチャのデッドロックフリー性の検証を行った。一般に並行プロセスのデッドロックフリー性の検証では公平性制約を課す必要があるが、公平性制約のもとでの検証は非常に時間がかかる。そこで、タスク制御アーキテクチャの構造に着目して公平性制約を用いずにデッドロックフリー性を検証する方法を示し、これにより100倍以上の高速化を達成できることが判明した。
|
