| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2015: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| 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.
|
