|
本研究では、実用規模の有限状態システムの形式的設計検証のための基礎的な手法の確立を目指して、時相論理の記号モデル検査法に基づく検証手法の研究を中心に行ない、主として以下の成果を得た。
1.記号モデル検査アルゴリズム: 時相論理の記号モデル検査法の基本演算である逆像計算を従来の用法よりも高速に計算するアルゴリズムを示した。実際に8ビットマイクロプロセッサの検証に適用した結果、従来法に比べて平均で10倍程度、最高で60倍近く高速化できることを示した。
2.時空間様相論理: ピットスライス構造を持つシステムを、時間方向と空間方向の2種類の状態遷移を含む有限状態システムとしてモデル化し、その仕様記述言語として時間方向と空間方向の性質を記述できる時空間様相論理の体系を提案しその記号モデル検査アルゴリズムを示した。
3.実時間システムの検証: 実時間システムの検証のための基礎的なアルゴリズムとして、2つのイベント間の遅延時間の上限と下限を正確に求めるシンボリックアルゴリズムや、一定の期間の間にあるイベントの発生回数の上限と下限を正確に求めるシンボリックアルゴリズムを示した。実際に、これらのアルゴリズムを用いて10^<15>状態の航空管制システムの検証を行ない、その有効性を示した。
4.16ビットマイクロプロセッサの検証: 16ビットマイクロプロセッサの検証を可能とする抽象化手法の研究を行い、データ幅の抽象化や一部の信号線の値を固定にすることが有効であることが判明した。これらの抽象化手法により、16ビットマイクロプロセッサの検証が可能となった。
|
