2016 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 | 形式仕様アニメーション / テストデータの自動生成 / 形式仕様記述技術 / データアニメーション / 形式仕様妥当性の検証 |
|---|
| Outline of Annual Research Achievements |
平成28年度では、次の三つの研究を行った。
1. テストに基づく形式仕様の自動検証手法について研究を行った。この手法で形式仕様に関する性質を表現する定理を自動的に検証することができる。定理に含まれるエラーが早く発見されることができ、エラーがない場合、その定理の正しさに対する確信に証拠を提供できる。また、この手法を形式仕様の整合性と妥当性の検証プロセスに統合して、形式仕様の整合性の検証を自動的に行うことができ、妥当性の検証を半自動的に実施することもできる。
2. 単独の操作の形式仕様の自動アニメーション用のテストデータの自動生成手法を提案した。事前条件と事後条件から形成された機能シナリオをアニメーション化するために、入力変数と出力変数のテストデータが自動的に生成され、それを用いて、操作の入力と出力間の対応関係を動的に表現することができる。この中で、特に、複合データ型の演算子を含む原子述語、論理積、および論理和など述語論理式から適切なテストデータを生成する基準と方法を確立した。
3. 単独操作の振る舞いをその操作の形式仕様によって動的に表現するために、データアニメーション、入出力関係のアニメーション、および形式仕様に使われる様々な演算子の意味を表現するアニメーションの手法を研究した。操作の入力データの性質や特徴を動的な分かりやすい表現によって、ユーザにそのデータに関するあらゆる面を理解させる。操作の入出力間の関係を、形式仕様に基づく自動的に生成されたテストデータを用いて、どんな入力によってどんな出力を生成できるかを分かりやすく表現する。また、ユーザ或いは別な開発者に形式仕様の表現を理解してもらうために、各データ型に定義された演算子の一部のアニメーションを作る。それによって、ユーザが形式表現の意味をはっきり理解することができる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成28年度の研究計画を作成した時に、研究課題、研究方法、および達成する目標を明確に理解しており、平成28年度において、研究グループの研究者の協力を得て、全力で計画した研究を実施した。その結果、SpringerのLNCSシリーズで二冊の研究論文集を出版、国際会議で6件の査読付き論文を公表、英文のジャーナルで論文一件を発表、国内会議で論文三件を発表、および国際会議で基調講演も行った。更に、東京で二つの国際会議ICFEM2016とSOFL＋MSVL2016を開催し、本研究の成果を世界の研究者に紹介し、解決していない課題について他の研究者と議論して解決策を調べた。
|
| Strategy for Future Research Activity |
平成29年度では、次の課題に集中して研究を行う。
1. 形式仕様記述過程のモニタリングと予想方法を研究する。形式仕様記述過程のモニタリングでは、作成した形式仕様の内容を随時チェックができ、エラーの早期発見と予防することができる。形式仕様記述の予想では、今まで作成した仕様の内容に基づき、これから作成すべき内容を予想して、ユーザに適切に推薦する。この手法によって、形式仕様記述過程にエラーを減らす、仕様作成効率を向上させることが期待される。
2. 形式仕様に基づく実装したプログラムのテストを行うために、以前の研究で提案した「振動テスト」手法を更に発展し、プログラムのパスを効率的に実行させるテストデータの生成方法と支援ツールを研究開発する。そのテストデータの生成手法を小規模の実験によって評価する。
3. 形式仕様によってハイブリッド仕様記述技術を開発する。この技術によってソフトウェア開発の要求分析と設計をより効率的に実現でき、ユーザが開発プロセスに参加することも可能であり、アジャイル形式工学手法の目標の実現に貢献できる。
4. 単独な操作の形式仕様のアニメーション化手法を提案し、支援ツールの研究開発を行う。SOFL形式仕様記述言語に定義された各データ型の演算子の振る舞いのアニメーション手法に基づき、論理式全体のアニメーションを行う手法と支援ツールを研究開発する。
|
