複数モジュールにより構成される回路仕様に対する効率的な形式的検証法

概要

論文の詳細を見る
複数モジュールにより構成される回路仕様に対する, 一つの効率的な形式的検証法を提案する. 各モジュール及び回路全体は, 拡張有限状態機械でモデル化する. 複数モジュールにより構成される回路仕様記述法の一つとして, 文脈自由ネットワーク文法とよばれる文法の形で表す方法を提案する. この文法は, 生成規則により回路の仕様記述を帰納的に行うことができる. 本手法では, 回路に対して抽象度の異なる二つのレベルを考える. 生成規則は, 要求仕様のレベルでは終端記号が表す回路の機能を追加することを表し, 実現仕様のレベルでは, 終端記号が表す具体的なモジュールを追加すること等の構造を表す. 検証は, 実現仕様が要求仕様を正しく実現していることを生成規則に従って帰納的に証明する. しかし, 検証は追加される差分のみで行なうのではなく, 回路全体の等価性を議論するのであるから, 具体的な, かつ, それほど大きくない全構成を与えなければ検証は実際上不可能である. 本手法では, 検証を効率的に進めるため, 1) 要求仕様, 実現仕様は同じ形の文法を用いる, 2) モジュールが線形に接続された構造を持つように生成規則を限定する, 3) 要求仕様と実現仕様の間の対応関係を設計者が与える, という3つの制限を加える. この文法から生成される回路の例としてn個のデバイスが接続できるバスシステムをとりあげる.
社団法人電子情報通信学会の論文
1997-10-29

複数モジュールにより構成される回路仕様に対する効率的な形式的検証法

スポンサーリンク

概要

著者

関連論文

スポンサーリンク