2016 Fiscal Year Annual Research Report
Research on Complexity Distribution and Consistency Assurance in Stepwise Refinement
| Project/Area Number |
26700005
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
石川 冬樹 国立情報学研究所, コンテンツ科学研究系, 准教授 (50455193)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | ソフトウエア開発効率化・安定化 / 形式手法 / システムモデリング / 段階的詳細化 / 定理証明 / Event-B |
|---|
| Outline of Annual Research Achievements |
ソフトウェアの効率的な信頼性確保のためには，抽象的な仕様の時点でのモデル化や検証が重要であるが，近年のシステムは仕様の時点でも複雑になっている．これに対し，概念や要件を徐々に導入，検証する段階的詳細化が有効である．しかし，理解や検証の容易性，および様々な種類の整合性を考慮しつつ，適切に導入対象や導入順序を決めることは難しい．これに対し本研究では，概念や要件間の依存関係に応じて，どう複雑さが分散されるかといった側面を定式化する．これにより，段階的詳細化の計画の良し悪しに関する知見，および適切な計画を導く手法を確立することを目指す．
本研究では，形式手法Event-Bを対象として，段階的詳細化の計画や，その複雑さおよび整合性に関する定式化に取り組んだ．次にこの定式化に基づき，プランニング手法およびリファクタリング手法，すなわち初めてモデルを構築するときの段階的詳細化の設計を行う手法と，以後にその設計を変更するための手法を確立した．特にリファクタリング手法については，その有用性が高いと考えられたため，Event-Bの支援ツールプラットフォームであるRODINのプラグインとしてツール実装を行った．また様々な実証評価により，理解容易性や検証容易性，再利用性の向上に有効であることを示した．そのほか，形式手法を必ずしも用いない場合として，要求分析手法としてよく知られるプロブレムフレームを対象とした手法も構築した．
|
