2017 Fiscal Year Annual Research Report
Research on Highly Reliable Agile Formal Engineering Methods
| Project/Area Number |
26240008
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
劉 少英 法政大学, 情報科学部, 教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
児玉 靖司 法政大学, 経営学部, 教授 (30266910)
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
荒木 啓二郎 九州大学, システム情報科学研究院, 教授 (40117057)
|
|---|
| Project Period (FY) |
2014-06-27 – 2019-03-31
|
| Keywords | 形式仕様アニメーション / 形式仕様作成の監視 / 形式仕様作成の予測 / アニメーションデータの自動生成 / データ項目のアニメーション / データ項目のGUI表現 |
|---|
| Outline of Annual Research Achievements |
平成29年度では、次の研究を行った。
１．今まで提案した形式仕様アニメーション用のテストデータの振動生成方法の支援ツールのプロトタイプを開発し、それによって振動生成方法の有効性を評価する実験を行った。その結果によると、この振動生成方法は既存のランダム生成方法より有効性が高い。但し、振動幅の基準の決め方に関しては課題がまだ残っている。これは今後研究の焦点の一つになる。
２．形式仕様の事前条件と事後条件を作成するプロセスの中でエラーを防止するための技術を提案した。この技術は、二つの部分から構成された。一つは形式仕様の作成するプロセスを監視しながら、導入されたエラーを検出する技術である。基本アイディアは、プログラムの内容から前提条件と結論を表現する定理を形成して、定理の自動テスト技術を適用することによってエラーを検出することである。もう一つは形式仕様の作成の中で、既存の内容によって期待される新しい内容を予測する技術である。基本的な技術は、形式仕様の最初の機能シナリオをユーザに書いてもらって、そのシナリオ中の論理関係によってほかの機能シナリオを予測することである。
３．形式仕様アニメーションで操作機能を表現するために、関連する様々な型のデータ項目のアニメーション方法と支援ツールのプロトタイプを開発した。この方法によって、データ項目の意味を分かりやすく解釈することができ、そのデータ項目の具体的な値を分かりやすい形で入力と出力するためのGUI表現の自動生成もできる。
４．今までの研究で提案したGUI補助する形式仕様作成の三段階技術の有効性を評価するために、小規模の実験を実施した。その結果、この三段階技術のメリットと課題を見つけて、今後の研究の材料になっている。
５．モデル検査をより分かりやすい形で行うために、検査プロセスおよび反例のアニメーション技術と支援ツールのプロトタイプを研究開発した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今までの研究内容を深く把握しており、本研究の研究者の協力を得て、計画した研究を全力で行ってきた。既存の難しい課題と新しく発見した課題に関しては、平成29年度に参加した様々な国際会議を通じて、世界中の優秀な研究者と幅広く議論することによって課題の解決の道筋を明らかにしている。また、本研究の研究者は、優秀な大学院生と一緒に研究を行い、支援ツールの開発や提案した技術の有効性の評価実験などを効率的に実施することによって、いろいろな役に立つ結果が出てきた。それらの結果によって、沢山の論文を作成し、国際会議で発表してきた。同時に、形式仕様によるテストデータの自動生成および操作の形式仕様のアニメーション技術に関わる成果をまとめて、IEEE TSEとACM TOSEMなどソフトウェア工学分野のトップレベルの論文誌へ投稿した。このような論文を作成しながら研究活動を推進する方法で計画した研究を効率的に行うことができた。
|
| Strategy for Future Research Activity |
平成30年度では、次の研究を行う予定である。
１．今までの研究で得た形式仕様アニメーション手法と形式仕様およびプログラムのエラーを検出するための定理のテスト検証手法の支援ツールの開発を続ける。
２．今までの研究によって確立した様々な仕様アニメーション技術と定理検証の技術の有効性を評価する実験を行う。大学院生と優秀な学部生からの協力を得てこのような実験研究を推進することを考えている。
３．今までの研究で得た結果をまとめて高いレベルの学術論文を作成し、ソフトウェア工学分野の論文誌と国際会議および国内会議へ投稿する。また、本研究の成果を社会に紹介するために必要な資料も作成する。
４．国際機関と国際会議の学術的な場で本研究の成果を紹介して、優れた研究者と幅広く議論する。これによって本研究で提案したアジャイル形式工学手法の確立という目標を達成するために解決しなければならない課題を発見し、できるだけ本研究の期間内で対応策を明らかにする。
|
