| 研究課題/領域番号 |
26700005
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
石川 冬樹 国立情報学研究所, コンテンツ科学研究系, 准教授 (50455193)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | ソフトウエア開発効率化・安定化 / 形式手法 / Event-B / 段階的詳細化 / Assurance Case |
|---|
| 研究実績の概要 |
ソフトウェアの効率的な信頼性確保には，抽象的な仕様の時点でのモデル化や検証が重要であるが，仕様の時点でも非常に複雑であることが多い．このため，概念や要件を徐々に導入，検証する段階的詳細化が必要であるが，理解や検証の容易性，および様々な整合性を考慮しつつ，適切に導入対象や導入順序を決めることは難しい．これに対し本研究では，概念や要件間の依存関係に応じ，どう複雑さが分散されるかといった側面を定式化する．これにより，段階的詳細化の計画の良し悪しに関する知見，および適切な計画を導く手法を確立することを目指す．
平成27年度は形式仕様記述のための手法Event-Bを対象として取り組みを行った．上述のように，Event-Bにおける様々な要件，概念，依存関係を整理し，段階的詳細化の計画やその複雑さに関する定式化を行った．またこの定式化を基にして，与えられた問題に対して段階的詳細化の計画の可能な設計空間を得て，設計指針に応じて計画立案を行うための手法およびプロトタイプツールを構築した．この手法・ツールについて，Event-Bの書籍や産業界の協力者から得たいくつかの例題について試行と改良を行うとともに，手法の評価および，段階的詳細化の設計空間に関する分析を行った．その結果，対象とする問題における依存関係に応じて設計空間の広さが定まることを明らかに示すことができた．また，十分な問題の分析結果と典型的な設計指針を与えることで，段階的詳細化の自動計画立案も行うことができた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
当初平成27年度に実施予定であった評価の多くの部分について，前倒しして実施できている．
|
| 今後の研究の推進方策 |
平成27年度の成果を踏まえ，ツールの洗練，さらなる評価に取り組む．また当初の予定通り，Event-B固有の要素を取り除き，一般の形式手法や，Assurance Caseなど形式手法に限らない手法についても，手法を発展させ，知見を得ることを進めていく．
|
| 次年度使用額が生じた理由 |
当初謝金にて依頼する予定であった資料整理や実験等の補助作業について，所属機関経費によるインターン生への依頼が可能となったこと，研究代表者自身も取り組んだことから不要となったため．
|
| 次年度使用額の使用計画 |
当初の予定よりも評価実験において，題材，内容を多くして取り組むことを検討しているため，この補助作業のための謝金に充てる予定である．
|
