形式仕様を用いた部品検索における計算量低減
スポンサーリンク
概要
- 論文の詳細を見る
高信頼ソフトウェア開発にソフトウェア部品再利用を適用する際や大規模なソフトウェア部品リポジトリを扱う際には部品検索の健全性が重要である.健全性の高い部品検索としては要求を記述した形式仕様を検索キーとして,その検索キーを満たす仕様を持つ部品を得ることが考えられる.しかし,この部品検索は各部品毎に部品の仕様が検索キーを満たすかを定理証明で判定するため計算量が大きく実用的でない.本稿では形式仕様の字面の統一により定理証明による判定を文字列一致で近似的に行う部品検索手法を提案する.一般的に文字列一致の検索で健全性を向上させると完全性が損なわれるため,形式仕様の字面を統一することで完全性を向上させる.数学的な形式仕様には全てを明示しなくても推論によって暗黙的な記述得られるため,字面の統一では暗黙的な記述を明示する事で明示される記述を統一する.また,モデルの構成要素の多くは順不同であるため,字面の統一ではそれらの並びを統一する.我々は高信頼なソフトウェア部品自動生成と健全性の高い部品再利用を自動化したソフトウェア自動合成フレームワークを提案してきた.この自動合成フレームワークの部品検索に本稿で提案する部品検索を応用することで高信頼なソフトウェアを迅速かつ低コストに開発することが期待できる.
- 2011-07-14
著者
-
中村 丈洋
電気通信大学大学院情報通信工学専攻
-
織田 健
電気通信大学大学院情報通信工学専攻
-
織田 健
電気通信大学大学院情報理工学研究科総合情報学専攻
-
織田 健
電気通信大学情報理工学研究科総合情報学専攻
関連論文
- 再利用による自動コード生成を目的としたB Methodにおけるソフトウェアの部品化(形式手法(学生セッション))
- B Methodにおける自動コード合成フレームワークの提案
- 4Q-3 形式的なソフトウェア部品検索のための仕様からの特徴抽出(再利用,保守,学生セッション,ソフトウェア科学・工学)
- インターネット環境におけるコンピュータリテラシの教育
- B-006 機能に着目したソフトウェア部品の抽象化による特徴抽出(ソフトウェア,一般論文)
- 4Q-4 形式的なソフトウェア部品検索のための仕様からの特徴抽出(再利用,保守,学生セッション,ソフトウェア科学・工学)
- ソフトウェア測定形式化による妥当性検証手法(定量化・評価)
- B-050 多様な品質要求に応じたソフトウェア部品提供のためのリポジトリシステム(B.ソフトウェア)
- B-037 Zによる仕様記述と状態遷移規則の比較による誤り検出法(B.ソフトウェア)
- B-018 エンティティの振舞いに着目したZによる仕様記述と状態遷移規則の比較に基づく誤り検出法(B分野:ソフトウェア)
- 形式仕様を用いた部品検索における計算量低減
- B Methodにおける高信頼ソフトウェア部品自動生成
- 高信頼細粒度部品再利用による形式手法におけるソフトウェア合成