有限状態システムの形式的設計検証に関する研究

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05680285
• Research Institution: Kyoto Sangyo University
• Principal Investigator: 平石 裕実 京都産業大学, 工学部, 教授 (40093299)
• Keywords: 設計検証 / 形式的検証 / 時相論理 / 有限状態システム / 分散アルゴリズム / 抽象化

Research Abstract

実用規模の有限状態システムの形式的設計検証を目指して研究を行い、以下の成果を得た。
1.記号モデル検査アルゴリズムの研究:BRTLやCTL等の分岐時間モデルの時相論理の記号モデル検査アルゴリズムにおける基本演算である逆像計算法として、像を表す特性関数に対して次状態関数を再帰的に代入する方法を新たに提案した。これを自在の8ビットマイクロプロセッサの設計検証に適用して、従来の次状態関数を順次代入する方法と比較実験を行った結果、時間で約10倍、必要な記憶容量で約2倍性能が改善されることが判明した。また、状態集合のフロンティア集合を表す特性関数の簡単化の実験も行い、これにより記号モデル検査に要する時間が2割程度改善されることが判明した。
2.検証の高速分散アルゴリズムの研究:記号モデル検査の並列・分散アルゴリズムの基礎的研究を開始した。特に、最近入手が容易になってきている、数台から数十台程度のマルチCPUワークステーションや、数十台のワークステーションの分散環境での実行に適した高レベルの分散アルゴリズムの開発を目指している。
3.抽象化手法の基礎的研究:より大規模なシステムの形式的検証を行うためには、検証対象の抽象化が重要であるが、抽象化手法の評価を行うために16ビットマイクロプロセッサ設計検証を開始した。この設計検証を通じて、データパス系のビット幅の抽象化、レジスタ数やメモリ容量の抽象化手法の検討を行った。また、特にデータパス系のビット幅の抽象化に関して、数学的帰納法の適用の可能性の検討を開始した。

Research Products

• [Publications] 平石裕実: "Formal Verification of Single Phase Behavior of KUE-CHIP2 Microprocessor" New Advances in Computer Aided Design Z Computer Graphics. 2. 611-616 (1993)
• [Publications] 平石裕実: "An Efficient Inverse Image Computation Algorithm for Seguenfial Machine Verificafion" Proc.PRFTS'93. 91-95 (1993)