我々は、形式手法B-Methodの信頼性保証の枠組みを利用した、部品の再利用による高信頼ソフトウェア合成手法の研究をしている。
要求仕様を満たす部品を検索する際には、計算コスト削減の観点から文字列一致を用いる。
従来手法では、数学的に等価なモデルが文字列上で一致するように、モデルの制約条件を推論により書き換えていたが、書き換え規則の合流性は保証されていなかったため、等価なモデルでも文字列一致させられないことが多かった。
本研究では、合流性の保証された項書き換え規則を整備し、より幅広い表現を独自の正規形に統一する手法を提案する。
加えて、モデルの操作部分も正規化し、部品の再利用性向上を図る。