4L-01
モジュール構造と段階的詳細化を考慮した形式的ソフトウェア合成手法
我々は形式手法の一つのBメソッドで記述された既存ソフトウェアから生成した部品を再利用したソフトウェア合成手法を提案している。ここで、モジュール構造の対応と段階的詳細化の対応の独立した研究の統合が課題である。
従来のモジュール構造の対応は段階的詳細化を、段階的詳細化の対応はモジュール構造を考慮していなかった。これらの手法を統合すると合成できるソフトウェアの構造を全て網羅できるが、統合に伴い生じる新たな課題として、モジュール構造の性質と段階的詳細化の性質を併せ持つ詳細化途中から導入されるモジュールを考慮する必要がある。本発表では、上記の課題に対応した形式的ソフトウェア合成手法を提案する。
従来のモジュール構造の対応は段階的詳細化を、段階的詳細化の対応はモジュール構造を考慮していなかった。これらの手法を統合すると合成できるソフトウェアの構造を全て網羅できるが、統合に伴い生じる新たな課題として、モジュール構造の性質と段階的詳細化の性質を併せ持つ詳細化途中から導入されるモジュールを考慮する必要がある。本発表では、上記の課題に対応した形式的ソフトウェア合成手法を提案する。