（邦文）事例研究：組込みシステムの仕様検証とペアワイズ・テスト手法を用いた評価項目の生成

組込みシステムでは信頼性の確保が極めて重要である。信頼性は様々な形式手法を用いて確保できる。我々は開発製品に形式手法を適用して信頼性を検証する技術について研究している。本稿では実際の開発に形式手法を適用した事例を紹介し、そのアプローチと検証結果について説明する。本研究の目的は評価項目と呼ぶパラメータに対する制約を含む仕様の正当性を確認することであり、そのためにモデル検査と充足可能性判定を採用して検証を行った。本研究では仕様から形式モデルヘの変換ルールを設定したが、変換の一部は手動で行った。手動による変換は評価項目の生成を制限するため、ペアワイズ法を用いた検証パラメータの自動生成を試みた。最後に検証結果を提示する。形式手法の適用は現時点ではまだ予備段階にあり、製品の自動的な検証に向けて形式手法を発展させていきたいと考えている。