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

• Item type: Journal(1)
• 公開日: 2011-11-15
• タイトル: B Methodにおける高信頼ソフトウェア部品自動生成
• タイトル / 言語: en
• タイトル: Denepndable Software Component Generation with B Method
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 一般論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 電気通信大学大学院電気通信学研究科情報通信工学専攻
• 著者所属: 電気通信大学情報理工学研究科総合情報学専攻
• 著者所属: 電気通信大学情報理工学研究科総合情報学専攻
• 著者所属(英): en
• 著者所属(英): Graduate School of Infomation and Communication Engineering, The University of Electro-Communications
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, The University of Electro-Communications
• 著者所属(英): en
• 著者所属(英): Graduate School of Informatics, The University of Electro-Communications
• 著者名: 中村, 丈洋; 織田, 健; 西野, 哲朗
• 著者名(英): Takehiro, Nakamura; Takeshi, Oda; Tetsuro, Nishino
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ソフトウェア部品への形式仕様の付加は部品の再利用性向上に有効である．しかし，再利用によりソフトウェアを開発するためには大量の部品を用意する必要があり，それらに形式仕様を与えることは大きなコストを生じる．これに対して既存ソフトウェアから部品を生成する手法があるが，仕様と部品の整合性保証が不十分である．そこで，本稿では仕様との整合性を保証できる高信頼ソフトウェア部品を提案する．また，この高信頼ソフトウェア部品をB Methodで構築されたソフトウェアから自動生成する手法を提案する．提案する高信頼ソフトウェア部品は実装依存モデルと細分化実装で構成され，仕様として細分化モデルを持つ．細分化モデル，実装依存モデル，細分化実装はそれぞれB Methodのモデルと実装に対応した記述であり，B Methodの信頼性の定義に基づいて信頼性が定義される．この部品の信頼性の定義に基づいて部品自動生成手法を構築することで自動生成された細分化モデルが無矛盾であるための条件を明らかにし，また，実装依存モデルと細分化実装が常に整合性を満たすことを保証する．この自動生成により高信頼部品リポジトリを容易に構築することが可能になる．さらに，高信頼部品リポジトリを応用することでB Methodで記述された要求仕様に対してそれを満たす実装を出力する高信頼自動コード生成が期待できる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 52, 号 11, p. 2989-3007, 発行日 2011-11-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764