Research on Highly Reliable Agile Formal Engineering Methods

2018 Fiscal Year Final Research Report

• Project/Area Number: 26240008
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Hosei University
• Principal Investigator: LIU Shaoying 法政大学, 情報科学部, 教授 (90264960)
• Co-Investigator(Kenkyū-buntansha): 児玉 靖司 法政大学, 経営学部, 教授 (30266910) ; 緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991) ; 荒木 啓二郎 九州大学, システム情報科学研究院, 教授 (40117057)
• Research Collaborator: TAMAI tetsuo ; FUTATSUGI kokichi ; NAKAJIMA shin ; KUMENO fumihiro
• Project Period (FY): 2014-06-27 – 2019-03-31
• Keywords: アジャイル開発手法 / 形式工学手法 / ハイブリッド仕様 / 仕様アニメーション / ソフトウェアテスト / ソフトウェア検証 / ソフトウェア品質保証 / 高信頼ソフトウェア開発

Outline of Final Research Achievements

In this research, we have established a new technology known as SOFL Agile Formal Engineering Method that significantly improves the existing software development methods in terms of offering a great capability of enhancing both software productivity and reliability. Specifically, the technology includes the following aspects:
(1) a framework of the SOFL Agile Formal Engineering Method, (2) a new method for carrying out the animation of hybrid specifications, (3) a new method and the related algorithms for automatically generating test data for both specification animation and specification-based program testing, (4) a method for combining theorem proving with model checking and a tool support for model checking process animation, (5) prototypes of software tools to support the automatic test data generation for both specification animation and specification-based program testing.

Free Research Field

ソフトウェア工学

Academic Significance and Societal Importance of the Research Achievements

本研究はソフトウェアの進化による開発手法と形式仕様記述によるソフトゥエア開発手法を適切に統合することによって双方の利点を生かすことができ、実用性がより高い厳密的なソフトウェア開発手法を確立することで、ソフトウェア工学方法論を大きく前進させ、将来のソフトウェア工学の発展の新たな方向を示すことができ、学術的意義が大きい。
一方、このような新しいソフトウェア開発手法が企業で採用されることによって、IT産業の生産性を向上させることができ、開発されるソフトウェアの信頼性の確保も可能であるため、より安全安心なシステムと社会を構築することが可能になる。