Integration of Formal Methods for Seamless Software Developments

2014 Fiscal Year Final Research Report

• Project/Area Number: 24500035
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: AOKI Toshiaki 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
• Project Period (FY): 2012-04-01 – 2015-03-31
• Keywords: 形式手法 / モデル検査 / 形式仕様記述 / テスト / 車載ソフトウェア

Outline of Final Research Achievements

In this research, we proposed a method to integrate multiple formal methods to cover the whole of system development phases consisting of formal specifications, designs and implementations. In addition, we succeeded in applying the proposed method to the verification of a practical automotive operating system and showing its effectiveness. Formal methods are usually used in a part of the development phases for embedded systems like automotive operating systems, however; in our approach, we suceeded in covering the whole of the phases. The automotive operating system that we verified is a practical one. By showing the fact that formal methods could be successfully applied to the practical system, we expect that adopting formal methods in industries is accelarated and reliability and safety of systems are improved more and more.

Free Research Field

ソフトウェア工学