2016 年 2016 巻 KSN-019 号 p. 03-
コンポーネントベース開発においては,その可変性の検証が必要である.検証の必要性としては,あるコンポーネントの組み合わせによる不整合の検出や,コンポーネント選択の誤りの検出がある.また,コンポーネントに対して機能を追加した場合,システムのディペンダビリティ要求を満たすことを確認する必要がある. 本稿では,コンポーネント間の整合性検証とコンポーネントへの機能追加に対するディペンダビリティの確認のために,形式手法Event-B を用いた方法を提案する.また,提案手法によって,コンポーネント間の不整合の発見,バリアント選択の誤りの発見,および機能追加における問題を発見できることを明らかにする.