2010 Fiscal Year Annual Research Report
ソフトウェア開発の現場で使えるフォーマルメソッドに関する研究
| Project/Area Number |
21300009
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, システム情報科学研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
日下部 茂 九州大学, システム情報科学研究院, 准教授 (70234416)
大森 洋一 九州大学, システム情報科学研究院, 助教 (20309727)
持尾 弘司 九州大学, 文学部, 准教授 (60331013)
|
|---|
| Keywords | フォーマルメソッド適用 / ソフトウェア開発プロセス / 形式的システム記述 / 非形式的システム記述 / 形式手法導入方法 / 文書品質改善支援 / 形式手法人材育成 |
|---|
| Research Abstract |
本年度は、形式手法の新たな適用事例として、企業との連携のもとに、通信制御システムを対象として仕様書の品質を向上させることによるシステム品質の向上に取組んだ。併せて、これまでの適用事例から得られた知見を整理して、形式手法を企業の開発現場に導入し適用するための指針を具体的に提示して、論文、研究会、シンポジウム、セミナー、企業における研修会などで広く紹介した。特に、個々の開発現場で採用されている具体的なシステム開発プロセスと形式手法との関係および形式手法適用の効果について議論し、形式手法導入方法の具体化に関する指針を示した。また、VDM++に対して、形式手法の初学者が学習する際の注意点や知見を取りまとめて、形式手法を導入する際の障壁を低くするための有益な資料として提示した。
システム開発の現場での形式手法導入を支援するために、要求記述からフォーマルなモデル生成を補助するツールを作成し、ツールを利用した変換手順を提案するとともにその効果を評価した。また、複数のフォーマルなモデル、特に機能モデルと振舞いモデルを変換するアルゴリズムを提案し、多様な視点に基づく検証を容易にする手法を考案した。
形式手法導入の得失を実際のソフトウェア開発のプロセスデータに帰着させて明確化することにより、そのメリットをより理解しやすくすることで普及を促進するアプローチを試行した。また、開発の上流工程での設計に実行可能な形式仕様記述を用いた場合、その設計の確認や設計空間の探索を予算やスケジュールに応じて伸縮可能な方式で実行する、クラウド型大規模仕様実行フレームワークのプロトタイプを開発した。
|
