B Methodにおける自動コード合成フレームワークの提案
スポンサーリンク
概要
- 論文の詳細を見る
ソフトウェア開発の迅速化と高信頼化を目的として自動コード生成や形式手法が研究されてきた.自動コード生成は経験則に基づいた再利用と定理証明に基づく手法に大分される.しかし,経験則に基づく手法は実用的であるが信頼性を保つことが難しく,定理証明に基づく手法は信頼性は高いが計算量が大きく実用化に至らない.一方,形式手法は高信頼ソフトウェア開発に威力を発揮するが,自動化や再利用による開発支援が十分では無い.本稿では形式手法B Methodにおいて高信頼部品を自動生成,再利用することで高信頼な実装を自動合成する事を提案する.B Methodの仕様と実装はその整合性を定理証明によって保証されるため,定理証明済の仕様と実装を整合性を維持するよう細分化することで高信頼部品を生成する.この部品に対して形式仕様に基づく健全性の高い再利用を適用することで高信頼な自動コード生成が可能となる.本稿ではB Methodの証明責務に基づいて部品と生成コードの信頼性を定義することで提案するフレームワークが満たすべき性質を明確にし,それに基づいてフレームワークの概要を説明する.また,定性的評価によって提案フレームワークの有効性を示す.
- 2010-11-04
著者
-
中村 丈洋
電気通信大学大学院情報通信工学専攻
-
織田 健
電気通信大学大学院情報通信工学専攻
-
織田 健
電気通信大学大学院情報理工学研究科総合情報学専攻
-
織田 健
電気通信大学情報理工学研究科総合情報学専攻
関連論文
- 再利用による自動コード生成を目的としたB Methodにおけるソフトウェアの部品化(形式手法(学生セッション))
- B Methodにおける自動コード合成フレームワークの提案
- 4Q-3 形式的なソフトウェア部品検索のための仕様からの特徴抽出(再利用,保守,学生セッション,ソフトウェア科学・工学)
- インターネット環境におけるコンピュータリテラシの教育
- B-006 機能に着目したソフトウェア部品の抽象化による特徴抽出(ソフトウェア,一般論文)
- 4Q-4 形式的なソフトウェア部品検索のための仕様からの特徴抽出(再利用,保守,学生セッション,ソフトウェア科学・工学)
- ソフトウェア測定形式化による妥当性検証手法(定量化・評価)
- B-050 多様な品質要求に応じたソフトウェア部品提供のためのリポジトリシステム(B.ソフトウェア)
- B-037 Zによる仕様記述と状態遷移規則の比較による誤り検出法(B.ソフトウェア)
- B-018 エンティティの振舞いに着目したZによる仕様記述と状態遷移規則の比較に基づく誤り検出法(B分野:ソフトウェア)
- 形式仕様を用いた部品検索における計算量低減
- B Methodにおける高信頼ソフトウェア部品自動生成
- 高信頼細粒度部品再利用による形式手法におけるソフトウェア合成