B Methodにおける高信頼ソフトウェア部品自動生成

概要

論文の詳細を見る
ソフトウェア部品への形式仕様の付加は部品の再利用性向上に有効である.しかし,再利用によりソフトウェアを開発するためには大量の部品を用意する必要があり,それらに形式仕様を与えることは大きなコストを生じる.これに対して既存ソフトウェアから部品を生成する手法があるが,仕様と部品の整合性保証が不十分である.そこで,本稿では仕様との整合性を保証できる高信頼ソフトウェア部品を提案する.また,この高信頼ソフトウェア部品をB Methodで構築されたソフトウェアから自動生成する手法を提案する.提案する高信頼ソフトウェア部品は実装依存モデルと細分化実装で構成され,仕様として細分化モデルを持つ.細分化モデル,実装依存モデル,細分化実装はそれぞれB Methodのモデルと実装に対応した記述であり,B Methodの信頼性の定義に基づいて信頼性が定義される.この部品の信頼性の定義に基づいて部品自動生成手法を構築することで自動生成された細分化モデルが無矛盾であるための条件を明らかにし,また,実装依存モデルと細分化実装が常に整合性を満たすことを保証する.この自動生成により高信頼部品リポジトリを容易に構築することが可能になる.さらに,高信頼部品リポジトリを応用することでB Methodで記述された要求仕様に対してそれを満たす実装を出力する高信頼自動コード生成が期待できる.
2011-11-15

B Methodにおける高信頼ソフトウェア部品自動生成

スポンサーリンク

概要

著者

関連論文

スポンサーリンク