| 研究課題/領域番号 |
01550285
|
|---|
| 研究種目 |
一般研究(C)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報工学
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
平石 裕実 京都大学, 工学部, 助教授 (40093299)
|
|---|
| 研究分担者 |
荻野 博幸 京都大学, 工学部, 教務職員 (40144323)
石浦 菜岐佐 京都大学, 工学部, 助手 (60193265)
高木 直史 京都大学, 工学部, 助手 (10171422)
|
|---|
| 研究期間 (年度) |
1989 – 1990
|
| 研究課題ステータス |
完了 (1990年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
1990年度: 800千円 (直接経費: 800千円)
1989年度: 1,500千円 (直接経費: 1,500千円)
|
|---|
| キーワード | 時相論理 / 形式的検証 / 論理設計 / モデル検査 / 設計検証 / 仕様記述 / 正則集合 / 順序機械 / 共有二分決定グラフ / 記号シミュレ-ション |
|---|
| 研究概要 |
本研究では、時相論理に基づく形式的な論理設計検証のための基礎的な手法の確立を目的として研究を行ない、主として以下のような成果を得た。
形式的論理設計検証のための論理体系としては、時間の概念を陽に記述することができ充足可能性判定問題が決定可能である時相論理が近年利用されつつあるが、従来の命題時相論理では、有限状態機械の性質を充分に表現することは出来なかった。このため、有限状態機械の仕様を表現する能力を持つ時相論理として我々がすでに提案している正則時相論理について研究を行ない、形式的論理設計検証の立場から、種々のクラスの正則時相論理の体系化を行ないそれらの諸性質を明らかにした。また、実際に正則時相論理を利用して順序機械の設計検証システムを試作し、実用規模の順序機械の設計検証に対して正則時相論理が有効に利用できることを示すとともに、アルゴリズムの改良を行ない、より効率の良い順序機械の検証アルゴリズムを示した。一方、論理回路のタイミング検証を目的として、実時間時相論理を変数が取り扱えるように拡張し、それを用いたタイミング検証アルゴリズムを明らかにした。さらに、最新のス-パ-コンピュ-タを利用することにより、どの程度の規模の順序機械の検証が可能になるかを明らかにするために、分岐時間モデルの時相論理の一種であるComputation Tree Logic(CTL)のベクトル計算機に適した検証アルゴリズムを示し、実際に実験を行ない状態遷移数が百万以上の順序機械の検証が扱えることを示した。
|
