Mendeley出力
＜博士論文＞
FeliCa IC チップ開発への実行可能な形式仕様記述の実践に基づく設計・構成法の提案
| 作成者 | |
|---|---|
| 論文調査委員 | |
| 本文言語 | |
| 学位授与年度 | |
| 学位授与大学 | |
| 学位 | |
| 学位種別 | |
| 出版タイプ | |
| アクセス権 | |
| JaLC DOI | |
| 概要 | 組織的に開発を進める必要があるソフトウェア開発現場において,上流工程の文書を中心に多くの問題を抱えており,品質の高いシステムを組織的に効率よく開発することができる手法として,フォーマルメソッドが注目されている.フォーマルメソッドの利用に関して,3段階の適用レベルが示されることがあるが,そのうち,本論文では,形式仕様記述を行うレベル0の段階を扱う.レベル0の段階とは,証明までは行わないが,数学的な記...法を用いて厳密な仕様を記述する段階である.筆者らはFeliCa ICチップ開発を通してレベル0における形式仕様記述手法の適用の効果を得ることができた.しかしながら,Parnasは2010年に発表した論文の中で,フォーマルメソッドが実践的手法として広く利用されるような「当然の技術」として,開発現場に浸透していない点を指摘した.本論文では,「当然の技術」として産業界に浸透するための課題を分析し,形式仕様記述手法を適用する際に必要不可欠となる形式仕様記述手法の設計・構成法を提案する.形式仕様記述手法が広く利用されるためには,形式仕様記述手法の専門家ではない人が,形式仕様記述を読み,理解し,活用していく必要がある.つまり,そのような形式仕様記述を書くための技術と,活用するための技術が必要である.本論文では,以下の3つの提案を行う.1つ目は,理解容易性に優れた形式仕様を記述するための,形式仕様記述の設計・構成法の提案である.2つ目は,従来からある既に開発現場に浸透しているレビューやテスト手法といった検証技術を主体として,その中で形式仕様記述手法を活用していく方法の提案である.3つ目は,筆者らが使用してきた形式仕様記述手法では取扱いが難しかった,動的な振る舞いに関する検証方法の提案である.1つ目の,理解容易性に優れた仕様を記述するためには,HayesとJonesが指摘した「実行可能性の影響」とJacksonが指摘した「実装の影響」を考慮する必要がある.まず,「実行可能性の影響」とは,仕様アニメーションとして知られている方法により記述した仕様を動作させる場合,この「動かすこと」を仕様記述の目的に含めてしまうことにより,仕様の理解容易性に影響を与えるというものである.次に,「実装の影響」とは次のような課題である.一般に,「解決すべき問題」を定義した仕様と,「問題の解決方法」を定義した設計を分けることで,仕様策定者と設計者が分業して組織的に開発を行うことができると言われている.しかし, 実際には,この2つを分けることは容易ではないため,仕様書に「問題の解決方法」を含めてしまうことで,設計者を過剰に制約してしまうという課題である.「実行可能性の影響」も「実装の影響」も,仕様の記述が複雑になり,過剰に設計を制約してしまうことが課題である. これらの課題を解決するために,「実行可能性の影響」に対しては,仕様伝達部と非伝達部からなる仕様記述スタイルを提案する.「実装の影響」に対しては,仕様と設計において定義するデータ構造に着目した形式仕様記述の設計・構成法を提案する.2つ目の提案として,形式仕様記述手法の専門家ではない,様々なレビューの目的を持った読者にとって,読みやすい仕様について分析を行い,レビューの目的とテストの目的を考慮した仕様記述フレームワークを提案する.構造が簡潔な点とテストとの親和性の点で,ディシジョンテーブルの構造を用いる方法と,仕様の概要と詳細を区別して記述する方法を提案する.また,実際に,形式仕様記述から体系的にテスト項目を作成し,テスト項目とテストスクリプトの網羅性を機械的に検証する方法を提案する.3つ目は,形式仕様記述手法では取扱いが容易でない動的な振る舞いに関する課題に対して,同時並行に動作する動的な振る舞いをモデル検査を用いて検証する方法を提案する.本論文では,これらの形式仕様を記述するための方法と活用するための方法を提案することによって,形式仕様記述手法が,産業界において適用可能で有効な手法であることを開発実践を通して示した.続きを見る |
| 目次 | 第1章 序論 第2章 本研究において扱うフォーマルメソッドの適用における課題 第3章 関連研究 第4章 仕様と設計を分離する実行可能仕様の設計・構成法の提案 第5章 レビューとテストの用途を考慮した仕様記述フレームワークの提案 第6章 動的な振る舞いに関するモデル検査の適用 第7章 結論 |
詳細
| レコードID | |
|---|---|
| 査読有無 | |
| キーワード | |
| 報告番号 | |
| 学位記番号 | |
| 授与日(学位/助成/特許) | |
| 受理日 | |
| 部局 | |
| 所蔵場所 | |
| 所蔵場所 | |
| 所在記号 | |
| 注記 | |
| 登録日 | 2013.07.10 |
| 更新日 | 2023.11.21 |