形式仕様を用いた部品検索における計算量低減

• 中村 丈洋

• 織田 健

書誌事項

タイトル別名

• A reduction in computational complexity to search software component with formal specifications

抄録

高信頼ソフトウェア開発にソフトウェア部品再利用を適用する際や大規模なソフトウェア部品リポジトリを扱う際には部品検索の健全性が重要である．健全性の高い部品検索としては要求を記述した形式仕様を検索キーとして，その検索キーを満たす仕様を持つ部品を得ることが考えられる．しかし，この部品検索は各部品毎に部品の仕様が検索キーを満たすかを定理証明で判定するため計算量が大きく実用的でない．本稿では形式仕様の字面の統一により定理証明による判定を文字列一致で近似的に行う部品検索手法を提案する．一般的に文字列一致の検索で健全性を向上させると完全性が損なわれるため，形式仕様の字面を統一することで完全性を向上させる．数学的な形式仕様には全てを明示しなくても推論によって暗黙的な記述得られるため，字面の統一では暗黙的な記述を明示する事で明示される記述を統一する．また，モデルの構成要素の多くは順不同であるため，字面の統一ではそれらの並びを統一する．我々は高信頼なソフトウェア部品自動生成と健全性の高い部品再利用を自動化したソフトウェア自動合成フレームワークを提案してきた．この自動合成フレームワークの部品検索に本稿で提案する部品検索を応用することで高信頼なソフトウェアを迅速かつ低コストに開発することが期待できる．The soundness of component reuse is important to develop dependable software, and to choose needed compoent from fuge number of components. Using formal specifications is one of the sound component reuse approach. But this approach needs theorem proving to compare search key and specification of component, and the compoutational complexity of theorem proving is too difficult to search components. In this paper, we propose a sound component search by a string comparison between normalized mathematical formal speficications. Most string comparison decrease completeness of search, so we increase completeness by normalizing specifications. To normalize specifications, we propose restriction expansion which reasons implicit descriptions, propose model normalization to sort their constructs. Applying our proposal to an automated software component reuse, it'll make us enable to develop dependable software more rapidly and more easily.

収録刊行物

• 研究報告ソフトウェア工学（SE）

  研究報告ソフトウェア工学（SE） 2011 (3), 1-8, 2011-07-14

詳細情報

• CRID: 1573387451823503104
• NII論文ID: 110008583151
• NII書誌ID: AN10112981
• 本文言語コード: ja
• データソース種別:
  • CiNii Articles