情報処理学会 第80回全国大会講演要旨

形式手法の一種であるB Methodは、仕様を記述したモデルの無矛盾性の検証と、
モデルから実装へ詳細化する際の整合性の検証を支援できる。
B Methodの既存ソフトウェアから高信頼細粒度部品を生成および整備することで、部品再利用によるソフトウェア自動合成などへの応用が期待できる。
B Methodのモデルの代入は同時に実行される一方、実装の代入は逐次的に実行される。そのため、再利用性のために部品の粒度をあまりに細かく設定すると、部品の結合により得られる合成実装がモデルを満たさない場合がある。
本研究では、合成実装の機能を保証できる最小の部品粒度を提案する。