抄録
ソフトウェア部品への形式仕様の付加は部品の再利用性向上に有効である．しかし，再利用によりソフトウェアを開発するためには大量の部品を用意する必要があり，それらに形式仕様を与えることは大きなコストを生じる．これに対して既存ソフトウェアから部品を生成する手法があるが，仕様と部品の整合性保証が不十分である．そこで，本稿では仕様との整合性を保証できる高信頼ソフトウェア部品を提案する．また，この高信頼ソフトウェア部品をB Methodで構築されたソフトウェアから自動生成する手法を提案する．提案する高信頼ソフトウェア部品は実装依存モデルと細分化実装で構成され，仕様として細分化モデルを持つ．細分化モデル，実装依存モデル，細分化実装はそれぞれB Methodのモデルと実装に対応した記述であり，B Methodの信頼性の定義に基づいて信頼性が定義される．この部品の信頼性の定義に基づいて部品自動生成手法を構築することで自動生成された細分化モデルが無矛盾であるための条件を明らかにし，また，実装依存モデルと細分化実装が常に整合性を満たすことを保証する．この自動生成により高信頼部品リポジトリを容易に構築することが可能になる．さらに，高信頼部品リポジトリを応用することでB Methodで記述された要求仕様に対してそれを満たす実装を出力する高信頼自動コード生成が期待できる．Formal specifications help us to reuse software components. But it cost to write formal specifications for all of software components. Automated component generation by slicing existent software is proposed to reduce this cost. But it's not enough in component reliability. In this paper we propose dependable software components (DSC), which can be ensured to satisfy specifications, and propose automated dependable software component generation (DSCG). A DSC is constructed with an implementation dependent model (IDM) and a sliced implementation, and a DSC has sliced model as its specification. These are similar to model and implementation in the B Method, and we can generate proof obligation from them. So we can ensure the consistency of a DSC and its specification applying the B Method. In this paper, we ensure the dependability in two angle by constructing that based on definitions of the DSC's consistency. First, we prove that sliced models generated by the DSCG has no contradiction conditionally. Second, we express the sliced model generated by the DSCG is sure to satisfy the IDM. We'll able to synthesis dependable software by composite DSCs to satisfy requirement models in the B Method.