正則時相論理に基づく形式的論理設計検証に関する研究

1990 Fiscal Year Annual Research Report

• Project/Area Number: 01550285
• Research Institution: Kyoto University
• Principal Investigator: 平石 裕実 京都大学, 工学部, 助教授 (40093299)
• Co-Investigator(Kenkyū-buntansha): 荻野 博幸 京都大学, 工学部, 教務職員 (40144323) ; 石浦 菜岐佐 京都大学, 工学部, 助手 (60193265) ; 高木 直史 京都大学, 工学部, 助手 (10171422)
• Keywords: 時相論理 / 形式的検証 / 論理設計 / モデル検査

Research Abstract

本年度は、実際に正則時相論理に基づく形式的設計検証システムを試作し、検証アルゴリズムの評価改良を行なうとともに、新たに分岐時間正則時相論理の構築や、ベクトル計算機向きの検証アルゴリズムの研究を行ない、主に次の成果を得た。
(1)形式的論理設計検証システムの試作:順序機械上で直接検証を行なう直接モデル検査法や仕様の式を分解して検証を行なうアルゴリズムを示し、実際に形式的検証システムを試作した。ベンチマ-クテストの結果、昨年度のアルゴリズムに比べて速度で約5〜10倍、必要なワ-クメモリにおいても大幅な向上が得られた。
(2)論理設計検証用論理体系の研究:線形時間モデルに基づく正則時相論理より効率の良い検証アルゴリズムが存在する論理体系として分岐時間正則時相論理を新たに提案し、計算の複雑度が順序機械の大きさと仕様の式の長さの積に比例する検証アルゴリズムを示した。
(3)論理設計検証手法の研究:正則時相論理に対して、記号モデル検査法に基づく検証手法を示し、これにより複数の順序機械を組み合わせた場合に生じる状態爆発問題をある程度回避することが出来、これらの論理体系を大規模順序機械の検証にも適用出来る見通しが得られた。また、非同期順序機械の検証に関連して、実時間時相論理の拡張と時間付順序機械モデルによりタイミング検証を行なう手法を示した。
(4)ベクトル計算機による設計検証:分岐時間時相論理CTLのベクトル計算機向きのモデル検査アルゴリズムを示し、適用対象が順序機械の検証であることを考慮してアルゴリズムの改良を行ない、状態遷移数が百万程度の順序機械の検証がベクトル計算機で数分程度で行なえることを示した。

Research Products

• [Publications] 平石 裕実: "Vectorized Model Checking for Compatation Trec Logic" Proc.of the Workshop on Computer Aided Verification. I. (1990)
• [Publications] 浜口 清治: "Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity" Proc.of the Worksop on Computer Aided Verification. II. (1990)
• [Publications] 平石 裕実: "有限オ-トマトンと表現等価な正則時相論理とその論理 設計検証への応用" 情報処理学会論文誌. 31. 1134-1145 (1990)