我々は形式手法の一つであるBメソッドに基づき、細分化モデルと実装の対である部品の再利用によるソフトウェア合成手法を提案してきた。
この手法中で部品が不足した場合に、可能であればその細分化モデルの実装を自動生成する手法が提案されている。しかし、この手法では自動生成した部品の無矛盾性や整合性の検証を行っておらず、生成された部品の信頼性に課題があった。また部品の検証は結合後のソフトウェアの無矛盾性や整合性の検証に役立つ可能性がある。本発表では先行手法を発展させ、部品の生成と無矛盾性や整合性の検証を自動で行う手法を提案する。