• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2014 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 26240008
Research InstitutionHosei 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

平成26年度の研究計画によって、次の三つの研究を行って、相応の成果を達成した。
1.SOFL(Structured Object-Oriented Formal Language)形式仕様記述言語に基づいて、仕様のアーキテクチャと操作を定義するモジュールから導出された「システム機能シナリオ」の振る舞いを動的に表現しながら設計の詳細を検証する形式仕様の自動アニメーション化技術の基本原理を明らかにした。その中で、システム機能シナリオの自動導出アルゴリズムを開発し、機能シナリオの整合性を検証する仕様間のトレーサビリティーに基づく検査(inspection)技術を提案した。また、機能シナリオの妥当性を検証するために、使用検査とテストを統合した技術も提案した。
2.単独の操作の機能仕様によってアニメーション化するために、仕様テスト技術を研究した。特に、形式仕様の事前条件と事後条件に基づき、テスト条件の自動生成およびテストケースの自動生成アルゴリズムと支援ツールを中心として研究した。この研究を完成するためには平成27年度以降でも研究を続けることが必要であるが、今年度の研究でテストケースの自動生成方法をほぼ確立した。
3.システム機能シナリオによって形式仕様アニメーション化技術の支援ツールを研究開発してきた。具体的には、三つの側面が含まれている。(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

平成26年度の研究計画に書かれた次の全ての研究目標を達成し、高いレベルの論文誌と国際会議で6枚の論文を発表し、一つの国際会議で基調講演も行い、一つの国際ワークショップでも口頭発表し、第77回情報処理全国大会でも発表した。
(1)形式仕様の自動アニメーション化技術の基本原理の研究。このなかに、アニメーションの対象とする整合性を確保した機能シナリオの自動導出方法および機能シナリオの振る舞いの正当性を検証する方法の研究がふくまれている。
(2)自動アニメーション用のテストデータの自動生成方法
(3)機能シナリオのテスト条件の自動生成
(4)テスト条件を満たすテストデータの自動生成

Strategy for Future Research Activity

今後の研究の推進方策としては、まず平成27年度に計画した研究を行って、その目標を達成するように努力する。具体的には、次の研究を行う。
(1)形式仕様の作成を支援する仕様パターン技術と支援ツール
(2)仕様アニメーション化するために必要なテストデータの生成基準
(2)テスト基準を満たすテストデータの自動生成
平成28年度以降の研究に関しては、平成27年度の研究の完成度によって平成27年度末ごろ判断する。
また、本研究の学術性と研究成果の実用性を向上させるためには、研究者の間により活発な議論、意見交換、および様々なレベルの研究協力を促進する。

  • Research Products

    (9 results)

All 2015 2014

All Journal Article (6 results) (of which Peer Reviewed: 6 results,  Open Access: 6 results,  Acknowledgement Compliant: 4 results) Presentation (3 results) (of which Invited: 1 results)

  • [Journal Article] Integrating Animation-Based Inspection into Formal Design Specification Construction for Reliable Software Systems2015

    • Author(s)
      Mo Li, Shaoying Liu
    • Journal Title

      IEEE Transactions on Reliability

      Volume: 印刷中 Pages: 印刷中

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Reviewing Formal Specification for Validation Using Animation and Trace Links2014

    • Author(s)
      Mo Li, Shaoying Liu
    • Journal Title

      Proceedings of 21th Asia-Pacific Software Engineering Conference (APSEC 2014), IEEE Press

      Volume: なし Pages: 286-293

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Tool Support for Rigorous Formal Specification Inspection2014

    • Author(s)
      Mo Li, Shaoying Liu
    • Journal Title

      Proceedings of IEEE 17th International Conference on Computational Science and Engineering (CSE 2014), IEEE Press

      Volume: なし Pages: 729-734

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Adopting Variable Dependency in Animation for Presenting the Behavior of Process2014

    • Author(s)
      Mo Li, Shaoying Liu
    • Journal Title

      Proceedings of 4th International Workshop on SOFL + MSVL, LNCS 8979, Springer

      Volume: なし Pages: 81-93

    • Peer Reviewed / Open Access
  • [Journal Article] Development of a Software Tool to Support Traceability-Based Inspection of SOFL Specifications2014

    • Author(s)
      Jinghua Zhang, Shaoying Liu
    • Journal Title

      Proceedings of 4th International Workshop on SOFL + MSVL, LNCS 8979, Springer

      Volume: なし Pages: 32-46

    • Peer Reviewed / Open Access
  • [Journal Article] Integrating Animation into Informal Specification Writing for Requirements Analysis2014

    • Author(s)
      Shaoying Liu, Fauziah binti Zainuddin, and Mo Li
    • Journal Title

      Proceedings of 3rd International Conference on Informatics Engineering and Information Science (ICIEIS 2014), SDIWC

      Volume: なし Pages: 136-143

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Presentation] 形式仕様に基づくテストケース自動生成2015

    • Author(s)
      池田逸人、劉少英
    • Organizer
      情報処理学会第77回全国大会
    • Place of Presentation
      京都大学(京都市)
    • Year and Date
      2015-03-17 – 2015-03-19
  • [Presentation] Integration of Specification Animation and SOFL Three-Step Specification Approach for Requirements Engineering2014

    • Author(s)
      Shaoying Liu
    • Organizer
      4th Asian Workshop of Advanced Software Engineering (AWASE 2014)
    • Place of Presentation
      Beijing (China)
    • Year and Date
      2014-10-11 – 2014-10-12
  • [Presentation] Testing-Based Formal Verification: A New and Practical Approach for Software Quality Assurance2014

    • Author(s)
      Shaoying Liu
    • Organizer
      19th International Conference on Engineering of Complex Computer Systems (ICECCS 2014)
    • Place of Presentation
      Tianjin (China)
    • Year and Date
      2014-08-04 – 2014-08-07
    • Invited

URL: 

Published: 2016-06-01  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi