2017 Fiscal Year Annual Research Report
Flexible Refactoring and Effective Guiding of Stepwise Refinement Design
| Project/Area Number |
17H07323
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
小林 努 国立情報学研究所, 大学共同利用機関等の部局等, 特任研究員 (10803405)
|
|---|
| Project Period (FY) |
2017-08-25 – 2019-03-31
|
| Keywords | 段階的詳細化 / 形式手法 / ソフトウェアモデリング |
|---|
| Outline of Annual Research Achievements |
複雑なソフトウェアシステムを数学的手法で厳密に検証する必要性が高まっている。そこで、ソフトウェアの形式モデルを複数の抽象度にわたって構築し、対象システムの構成要素を段階的に導入しつつモデルを検証する手法(段階的詳細化)が注目されている。このアプローチはモデルの保守・発展性の向上に貢献する可能性を秘めるが、その恩恵の大きさは導入される要素と導入の順序の選び方に大きく左右される。しかし、適切な要素やその導入順序を事前に選ぶことは難しい。
そこで本研究では、既存のモデルで導入されている要素や導入の順序を、モデルの整合性を保ちつつ自動で柔軟に変更する手法を構築する。さらに、提案手法を用いて様々な導入順に関して比較実験を行い、状況に応じた適切な導入順を選ぶための指針を確立する。これにより、既存のモデルで行われている詳細化を改良でき、形式モデルの保守・発展性を向上できるという点で本研究の意義は大きい。
平成29年度においては、新しい要素を既存のモデルに追加する手法の構築に取り組んだ。
そのためにまず、ソフトウェア開発における問題の分析手法の図式を利用し、形式モデル上の詳細化パターンを実問題の図式に対応させる手法を構築した。これにより、ユーザが本手法を利用する際に直観的な指示を与えられるようになった。次に、モデルに新しく記述を導入した際に、既存の記述と整合性を持たせるために必要な補助的な記述を導出する手法を構築した。これにより、パターン由来の記述が不適切なものでないならば、元のモデルの整合性を崩すことなく記述を導入できるようになった。さらに、補助的な記述の導出や、パターン由来の記述を用いたモデルの変更の自動化を進めた。これにより、手法の実用性が向上した上、平成30年度に実施予定の比較実験の準備を進められた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究における目標は以下の5つである。
1. 形式モデル上の詳細化パターンを実問題の図式に対応させる手法の構築 2. 新しい記述と既存の記述との整合性を持たせるための記述の導出手法の構築 3. 実モデルの分析による、保守・発展に効果的であることが経験的に知られているパターンの獲得 4. モデルの変更の自動化 5. モデルに様々な変更を施した結果の比較を通じた分析
申請時の予定は、平成29年度に目標1,2,3を、平成30年度に目標4,5を達成するというものだった。しかし、平成29年度の研究遂行を通じ、実モデルの分析を通じて得られたパターンをモデルとして具体化して確認することが適切なパターンの定義(目標3)のために必要であり、そのためには目標4を先に達成することが研究の遂行上望ましいと判断した。
そこで当初の計画を変更し、平成29年度に目標1,2,4を、平成30年度に目標3,5を達成することにし、変更後の計画に従って研究を遂行した。
以上より、目標達成の一部の順序に入れ替わりはあるものの、研究の進捗はおおむね予定通りと考えて良いと思われる。
|
| Strategy for Future Research Activity |
平成30年度では、平成29年度の成果をもとに、研究の目標のうち実験と分析に関わるもの、すなわち目標3,5の達成を目指す。
目標3(実モデルの分析による、保守・発展に効果的であることが経験的に知られているパターンの獲得)：公開されている多段階形式モデルを分析し、特に複数のモデルの要素間の関係について記述した式の形に着目して、パターンの定義を行う。
目標5(モデルに様々な変更を施した結果の比較を通じた分析)：あるモデルMについて、モデルの要素の導入の順序や粒度について、Mで採用されているもの以外にも様々な可能性が考えられる。目標4で達成した自動化手法を用いて、モデルMに対し様々な詳細化の変更を施した新しいモデルM'1, M'2, ...を構築する。そして、得られたモデルを比較し分析することで状況に応じた適切な導入順を選ぶための指針を確立する。
|
