文献

J-GLOBAL ID：201502262370461175   整理番号：15A0475996

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

Software Synthesis in Formal Method by Reusing Dependable Fine-grained Component

著者 (3件)： 中村丈洋 (電通大 大学院電気通信学研究科) ,  織田健 (電通大 大学院情報理工学研究科) ,  西野哲朗 (電通大 大学院情報理工学研究科)
資料名： 情報処理学会論文誌ジャーナル(Web)
巻： 54  号： 8  ページ： WEB ONLY 2012-2024  発行年： 2013年08月15日 
JST資料番号： U0452A  ISSN： 1882-7764  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 部品再利用によるソフトウェア合成は開発コスト低減や信頼性向上に有効であるが,高信頼な部品の整備が容易でなく,また,適用可能な問題領域が限定される点が問題となる。本稿ではこの問題に対してモデル充足ソフトウェア合成(MSSS)を提案する。MSSSは形式手法B Methodの信頼性保証を応用したモデル充足細粒度部品に数学的判定による健全性の高い再利用を適用してソフトウェアを合成する。これにより部品の信頼性を静的に保証でき,また変数名や部品名の解釈に起因する誤りを排除できる。一方で変数名や部品名に意味を持たせないため,部品名での機能の呼び出しによる合成ができず,変数名の書き換えや結合が必要になる。よって,本稿ではMSSSの信頼性を‘モデル充足’として数学的に定義し,そこからMSSSの手順を定めることで,互いに矛盾しない部品群を再利用したソフトウェアがB Methodの信頼性を満たすことを保証する。また,MSSSでは要求仕様を一意の粒度に細分化して部品の仕様に対する検索キーとするため,検索キーを不足部品の仕様として提示でき,さらに,部品自動生成により部品を容易に整備できる。これにより,合成手法を適用可能な問題領域の拡大と,それによる高信頼ソフトウェア開発の低コスト化と迅速化が期待できる。(著者抄録)

シソーラス用語： *ソフトウェア開発 ,  *形式的手法【計算機】 ,  形式的仕様 ,  信頼性 ,  安全性 ,  性能評価 ,  製品開発 ,  品質管理 ,  粒度 ,  再利用 ,  計算機プログラム ,  自動プログラミング ,  充足可能性問題 ,  制約充足問題 ,  健全性 ,  要求仕様 ,  ソフトウェア再利用 ,  プログラム合成 ,  細粒度
準シソーラス用語： 高信頼性 ,  充足問題 ,  制約充足

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

引用文献 (14件)：

• Manna, Z. and Waldinger, R.: Toward automatic program synthesis, Comm. ACM, Vol.14, No.3, pp.151-165 (1971).
• Greenfield, J., Short, K., Cook, S. and Kent, S.: Software Factories: Assembling Applications with Patterns, Models, Frameworks, and Tools, Wiley (2003).
• CEA: Papyrus UML, available from (http://www.papyrusuml.org/) (accessed 2010-12).
• Abrial, J.: The B-Book, Cambridge University Press (1996).
• 中村丈洋,織田健,西野哲朗:B Methodにおける高信頼ソフトウェア部品自動生成,情報処理学会論文誌,Vol.52,No.11,pp.2989-3007(2011).

タイトルに関連する用語 (4件)： 細粒度 ,  再利用 ,  形式手法 ,  ソフトウェア