高信頼細粒度部品再利用による形式手法におけるソフトウェア合成

• Item type: Journal(1)
• 公開日: 2013-08-15
• タイトル: 高信頼細粒度部品再利用による形式手法におけるソフトウェア合成
• タイトル / 言語: en
• タイトル: Software Synthesis in Formal Method by Reusing Dependable Fine-grained Component
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文] 再利用，高信頼，自動合成，B Method
• 資源タイプ / 資源タイプ識別子: 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
• 論文抄録 / 内容記述: 部品再利用によるソフトウェア合成は開発コスト低減や信頼性向上に有効であるが，高信頼な部品の整備が容易でなく，また，適用可能な問題領域が限定される点が問題となる．本稿ではこの問題に対してモデル充足ソフトウェア合成（MSSS）を提案する．MSSSは形式手法B Methodの信頼性保証を応用したモデル充足細粒度部品に数学的判定による健全性の高い再利用を適用してソフトウェアを合成する．これにより部品の信頼性を静的に保証でき，また変数名や部品名の解釈に起因する誤りを排除できる．一方で変数名や部品名に意味を持たせないため，部品名での機能の呼び出しによる合成ができず，変数名の書き換えや結合が必要になる．よって，本稿ではMSSSの信頼性を‘モデル充足’として数学的に定義し，そこからMSSSの手順を定めることで，互いに矛盾しない部品群を再利用したソフトウェアがB Methodの信頼性を満たすことを保証する．また，MSSSでは要求仕様を一意の粒度に細分化して部品の仕様に対する検索キーとするため，検索キーを不足部品の仕様として提示でき，さらに，部品自動生成により部品を容易に整備できる．これにより，合成手法を適用可能な問題領域の拡大と，それによる高信頼ソフトウェア開発の低コスト化と迅速化が期待できる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Software synthesis by reusing software components is effective to reduce development cost and to increase dependency. Nevertheless, it is not easy to prepare components, so domains to apply synthesis are limited. we must prepare components for each software domain to apply synthesis, and it's difficult to prepare dependable components. In this paper, we propose ‘Model Satisfiable Software Synthesis (MSSS)’ to resolve these problems. MSSS synthesises software by reusing ‘Model Satisfiable Fine-grained Component (MSFC)’ mathematically. We can ensure static dependability of MSFC by B Method. And mathematical reuse prevents bugs caused by misunderstanding of function name. However, MSSS needs intricate rewriting and combination to interlock MSFCs, because we can't reuse them by name of function. So we define mathematical dependency of MSSS as ‘model satisfiable’ to define procedure of it. MSSS slices requirement uniquely to search components by sliced requirement. So we can make lacked components easily by using search-keys as specification of them. And also we can generate MSFCs from existing software. MSSS will enable us to apply synthesis to more software domains, and to develop dependable software quickly in lower cost.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 54, 号 8, p. 2012-2024, 発行日 2013-08-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764