抄録
B-008
形式手法B Methodの細粒度部品の結合による高信頼ソフトウェアの合成
高橋宏夢・織田 健(電通大)
形式手法の一種であるB Methodは仕様を記述したモデルの無矛盾性や、モデルと実装間の整合性を検証できる。本研究ではB Methodに基づく細粒度部品の再利用および結合により、入力モデルを満たす高信頼実装を機械的に合成する手法を提案する。モデルの代入は同時に実行される一方、実装の代入は逐次的に実行されるため、部品結合の際は代入順序を考慮する必要がある。また、部品が操作呼び出しを行っている場合は状態の変化が明示的でないことがある。これらの課題に対し、入力モデルの記述を参照しつつ部品を適切に結合する手法を提案する。また、合成された実装が入力モデルを満たすことを保証する適切な粒度の部品を提案する。