Formal verification of advanced functionalities in next-generation automotive operating systems

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00094
• 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: Toshiaki Aoki 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
• Project Period (FY): 2015-04-01 – 2018-03-31
• Keywords: 形式手法 / 形式検証 / 車載システム / 形式仕様 / 定理証明

Outline of Final Research Achievements

We proposed methods to formally verify advanced functions of AUTOSAR operating system. Protection function and multicore function are provided for next generation cars in AUTOSAR operating system. Thus, we proposed practical methods to formally verify those functions. In the formal verification of the protection function, its formal specification was developed based on the specification of AUTOSAR operating system and we succeeded in finding the inconsistency of the AUTOSAR operating system specification during proving the consistency of the specification by theorem proving. In the formal verification of the multicore function, we proposed a method to automatically verify programs by automated theorem proving based on multiple memory models, and successfully verified spinlock programs of real operating systems such as Linux and TOPPERS/FMP.

Free Research Field

ソフトウェア工学