1K-01
小規模なモデルを対象とした形式的ソフトウェア合成システムの構築
○田中涼介,檜垣 廉,織田 健(電通大)
我々は形式手法の一つである B メソッドに基づき、細分化モデルと実装の対である部品の再利用によるソフトウェア合成手法を提案してきた。本研究ではシステム構築の第一歩として、単一の抽象機械によりモデル化されるソフトウェアのみを対象とする。本発表では、ソフトウェア部品の検索キーとするために定めた等価性判定に適した形にモデルを細分化する詳細な工程と、部品を格納するリポジトリの構造、さらに合成システム中で一貫した部品を表すデータ構造を提案する。また、個別に提案されてきた各工程のアルゴリズムを実装レベルに具体化し、連携させて構築したソフトウェア合成システムについて述べる。