• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2017 年度 実績報告書

ソフトウェア開発の高信頼アジャイル形式工学手法に関する研究

研究課題

研究課題/領域番号 26240008
研究機関法政大学

研究代表者

劉 少英  法政大学, 情報科学部, 教授 (90264960)

研究分担者 児玉 靖司  法政大学, 経営学部, 教授 (30266910)
緒方 和博  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
荒木 啓二郎  九州大学, システム情報科学研究院, 教授 (40117057)
研究期間 (年度) 2014-06-27 – 2019-03-31
キーワード形式仕様アニメーション / 形式仕様作成の監視 / 形式仕様作成の予測 / アニメーションデータの自動生成 / データ項目のアニメーション / データ項目のGUI表現
研究実績の概要

平成29年度では、次の研究を行った。
1.今まで提案した形式仕様アニメーション用のテストデータの振動生成方法の支援ツールのプロトタイプを開発し、それによって振動生成方法の有効性を評価する実験を行った。その結果によると、この振動生成方法は既存のランダム生成方法より有効性が高い。但し、振動幅の基準の決め方に関しては課題がまだ残っている。これは今後研究の焦点の一つになる。
2.形式仕様の事前条件と事後条件を作成するプロセスの中でエラーを防止するための技術を提案した。この技術は、二つの部分から構成された。一つは形式仕様の作成するプロセスを監視しながら、導入されたエラーを検出する技術である。基本アイディアは、プログラムの内容から前提条件と結論を表現する定理を形成して、定理の自動テスト技術を適用することによってエラーを検出することである。もう一つは形式仕様の作成の中で、既存の内容によって期待される新しい内容を予測する技術である。基本的な技術は、形式仕様の最初の機能シナリオをユーザに書いてもらって、そのシナリオ中の論理関係によってほかの機能シナリオを予測することである。
3.形式仕様アニメーションで操作機能を表現するために、関連する様々な型のデータ項目のアニメーション方法と支援ツールのプロトタイプを開発した。この方法によって、データ項目の意味を分かりやすく解釈することができ、そのデータ項目の具体的な値を分かりやすい形で入力と出力するためのGUI表現の自動生成もできる。
4.今までの研究で提案したGUI補助する形式仕様作成の三段階技術の有効性を評価するために、小規模の実験を実施した。その結果、この三段階技術のメリットと課題を見つけて、今後の研究の材料になっている。
5.モデル検査をより分かりやすい形で行うために、検査プロセスおよび反例のアニメーション技術と支援ツールのプロトタイプを研究開発した。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

今までの研究内容を深く把握しており、本研究の研究者の協力を得て、計画した研究を全力で行ってきた。既存の難しい課題と新しく発見した課題に関しては、平成29年度に参加した様々な国際会議を通じて、世界中の優秀な研究者と幅広く議論することによって課題の解決の道筋を明らかにしている。また、本研究の研究者は、優秀な大学院生と一緒に研究を行い、支援ツールの開発や提案した技術の有効性の評価実験などを効率的に実施することによって、いろいろな役に立つ結果が出てきた。それらの結果によって、沢山の論文を作成し、国際会議で発表してきた。同時に、形式仕様によるテストデータの自動生成および操作の形式仕様のアニメーション技術に関わる成果をまとめて、IEEE TSEとACM TOSEMなどソフトウェア工学分野のトップレベルの論文誌へ投稿した。このような論文を作成しながら研究活動を推進する方法で計画した研究を効率的に行うことができた。

今後の研究の推進方策

平成30年度では、次の研究を行う予定である。
1.今までの研究で得た形式仕様アニメーション手法と形式仕様およびプログラムのエラーを検出するための定理のテスト検証手法の支援ツールの開発を続ける。
2.今までの研究によって確立した様々な仕様アニメーション技術と定理検証の技術の有効性を評価する実験を行う。大学院生と優秀な学部生からの協力を得てこのような実験研究を推進することを考えている。
3.今までの研究で得た結果をまとめて高いレベルの学術論文を作成し、ソフトウェア工学分野の論文誌と国際会議および国内会議へ投稿する。また、本研究の成果を社会に紹介するために必要な資料も作成する。
4.国際機関と国際会議の学術的な場で本研究の成果を紹介して、優れた研究者と幅広く議論する。これによって本研究で提案したアジャイル形式工学手法の確立という目標を達成するために解決しなければならない課題を発見し、できるだけ本研究の期間内で対応策を明らかにする。

  • 研究成果

    (17件)

すべて 2018 2017

すべて 雑誌論文 (16件) (うち国際共著 1件、 査読あり 16件) 図書 (1件)

  • [雑誌論文] An Investigation of Integrating a GUI-Aided Approach and a Specification-Based Testing2018

    • 著者名/発表者名
      Fumiko Nagoya, Shaoying Liu
    • 雑誌名

      Proccedings of 7th International Conference on SOFL+MSVL (SOFL+MSVL 2017), LNCS 10795

      巻: - ページ: 24-35

    • 査読あり
  • [雑誌論文] A Software Tool to Support the "Vibration" Method2018

    • 著者名/発表者名
      Pan Zhao, Shaoying Liu
    • 雑誌名

      Proccedings of 7th International Conference on SOFL+MSVL (SOFL+MSVL 2017), LNCS 10795

      巻: - ページ: 171-186

    • 査読あり
  • [雑誌論文] A Software Tool to Support Scenario-Based Formal Specification for Error Prevention2018

    • 著者名/発表者名
      Siyuan Li, Shaoying Liu
    • 雑誌名

      Proccedings of 7th International Conference on SOFL+MSVL (SOFL+MSVL 2017), LNCS 10795

      巻: - ページ: 187-199

    • 査読あり
  • [雑誌論文] Assessing and Extracting Software Security Vulnerabilities in SOFL Formal Specifications2018

    • 著者名/発表者名
      Busalire Onesmus Emeka, Shaoying Liu
    • 雑誌名

      Proceedings of 2018 International Conference on Electronics, Information, and Communication (ICEIC 2018)

      巻: - ページ: 1-4

    • 査読あり
  • [雑誌論文] Graphically perceiving characteristics of the MCS lock and model checking them2018

    • 著者名/発表者名
      Tam Thi Thanh Nguyen, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 7th International Workshop on SOFL+MSVL (SOFL+MSVL 2017), LNCS 10795

      巻: - ページ: 3-23

    • 査読あり
  • [雑誌論文] A proof score approach to formal verification of an imperative programming language compiler2018

    • 著者名/発表者名
      Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 7th International Workshop on SOFL+MSVL (SOFL+MSVL 2017), LNCS 10795

      巻: - ページ: 200-217

    • 査読あり
  • [雑誌論文] A Comparative Study of a GUI-Aided Formal Specification Construction Approach2017

    • 著者名/発表者名
      Fumiko Nagoya, Shaoying Liu
    • 雑誌名

      Proceedings of 2017 International Conference on Computational Science and Its Applications (ICCSA 2017)

      巻: - ページ: 273-283

    • 査読あり
  • [雑誌論文] Security Requirement Engineering Using Structured Object-Oriented Formal Language for M-Banking Applications2017

    • 著者名/発表者名
      Busalire Onesmus Emeka, Shaoying Liu
    • 雑誌名

      Proceedings of 2017 IEEE International Conference on Software Quality, Reliability and Security (QRS 2017)

      巻: - ページ: 176-183

    • 査読あり
  • [雑誌論文] Semi-Formal Verification with Supporting Tool by Automatic Application of Hoare Logic2017

    • 著者名/発表者名
      Shingo Fukuoka, Yixiang Chen, Shaoying Liu
    • 雑誌名

      Proceedings of 4th Annual International Conference on Computer Science and Applications (CSA2017)

      巻: - ページ: 1-5

    • 査読あり / 国際共著
  • [雑誌論文] A Maude Environment for CafeOBJ2017

    • 著者名/発表者名
      Adrian Riesco, Kazuhiro Ogata, Futatsugi Kokichi
    • 雑誌名

      Formal Aspects of Computing, Springer (FAoC)

      巻: 29(2) ページ: 309-334

    • 査読あり
  • [雑誌論文] A Divide and Conquer Approach to Liveness Model Checking under Fairness & Anti-fairness Assumptions2017

    • 著者名/発表者名
      Kazuhiro Ogata
    • 雑誌名

      Frontiers of Computer Science (FCS)

      巻: - ページ: -

    • 査読あり
  • [雑誌論文] Model Checking the iKP Electronic Payment Protocols2017

    • 著者名/発表者名
      Kazuhiro Ogata
    • 雑誌名

      Journal of Information Security and Applications (JISA)

      巻: 36 ページ: 101-111

    • 査読あり
  • [雑誌論文] Specifying a Distributed Snapshot Algorithm as a Meta-program and Model Checking it at Meta-level2017

    • 著者名/発表者名
      Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 37th IEEE International Conference on Distributed Computing Systems

      巻: - ページ: 1586-1596

    • 査読あり
  • [雑誌論文] A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker2017

    • 著者名/発表者名
      Tam Thi Thanh Nguyen, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 7th Annual Conference on Software Analysis, Testing and Evolution (SATE 2017)

      巻: - ページ: 53-62

    • 査読あり
  • [雑誌論文] Graphical Animations of State Machines2017

    • 著者名/発表者名
      Tam Thi Thanh Nguyen, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 15th IEEE International Conference on Dependable, Autonomic and Secure Computing (15th DASC)

      巻: - ページ: 604-611

    • 査読あり
  • [雑誌論文] Writing concurrent Java programs based on CafeOBJ specifications2017

    • 著者名/発表者名
      Xuan-Linh Ha, Kazuhiro Ogata
    • 雑誌名

      Proceedings of 25th Asia-Pacific Software Engineering Conference (APSEC 2017)

      巻: - ページ: 618-623

    • 査読あり
  • [図書] Structured Object-Oriented Formal Language and Method; 7th International Workshop, SOFL+MSVL 20172018

    • 著者名/発表者名
      Cong Tian, Fumiko Nagoya, Shaoying Liu, Zhenhua Duan (eds)
    • 総ページ数
      219
    • 出版者
      LNCS 10795, Springer
    • ISBN
      978-3-319-90104-6

URL: 

公開日: 2018-12-17  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi