仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法

摘要

近年、設計期間を短縮するために設計資産の再利用がよく行われている。その際、異なるインタフェースを持つ設計同士を接続する場合にはプロトコル変換器を設計し挿入する必要がある。そのため、設計資産再利用を行う設計において、プロトコル変換器の設計と検証は重要である。そこで、本研究では、異なるプロトコルで通信するモジュール間を接続するプロトコル変換器の形式的検証手法を提案する。提案手法では、通信する双方のプロトコルの仕様の積を取ることにより、プロトコル変換器設計の仕様を得る。その後、シミュレーションによって、その仕様のうち設計において実装されている部分を抽出し、そこから設計が満たすべきプロパティを作成する。最終的に、このプロパティによって形式的検証を行い、全てのプロパティを満たせば設計の正しさを証明することができる。実験として、提案手法によるAMBAとOCPのプロトコル変換器に対する検証結果を示す。