1994 Fiscal Year Annual Research Report
| Project/Area Number |
05680285
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕実 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Keywords | 形式的設計検証 / 有限状態システム / 時相論理 / 記号モデル検査 / 論理設計検証 |
|---|
| Research Abstract |
本年度は、ビットスライス構造のシステムの検証を行なうための論理体系として時空間様相論理の研究や、応答時間や遅延時間の検証が必要な実時間システムの検証、また、より大規模な有限状態システムとして16ビットマイクロプロセッサの検証に関する研究を中心的に行ない、以下の研究成果を得た。
1.時空間様相論理:全く同じ構造を持つセルを一次元的に繰り返し接続するビットスライス構造のシステムの検証を行なうために、このようなシステムを、時間方向と空間方向の二方向の遷移システムとして抽象化したモデルを構築し、そのモデルの検証を行なう時空間様相論理体系を明らかにして、それに基づく検証アルゴリズムを示した。
2.実時間システムの研究:実時間システムの検証のための基礎的なアルゴリズムとして、2つのイベント間の遅延時間の上限と下限を求めるシンボリックアルゴリズムや、一定の機関の間にあるイベントの発生回数の上限と下限を求めるシンボリックアルゴリズムを示した。
3.16ビットマイクロプロセッサの検証:昨年度示した検証アルゴリズムでは、必要な記憶容量の点から16ビットマイクロプロセッサの検証は困難であることが判明したので、データ幅を8ビットに抽象化し、信号線の一部を固定化することにより検証が可能になることを示した。
|
-
[Publications] 平石裕実: "論理関数処理に基づく形式的検証手法" 情報処理. 35. 710-718 (1994)
-
[Publications] H.Hiraishi: "Time-Space Modal Model Checking towards Verification of Bit-Slice Architecture" Proc.3rd Asian Test Symp.287-291 (1994)
-
[Publications] S.V.Campos: "Computing Quantitative Characteristics of Finite-State Real-Time Systems" Proc.Real-Time System Symp.266-270 (1994)
