2015 Fiscal Year Research-status Report
次世代車載オペレーティングシステムにおける先進機能の形式検証に関する研究
| Project/Area Number |
15K00094
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 車載システム / 形式仕様 / 形式検証 |
|---|
| Outline of Annual Research Achievements |
平成２７年度は，AUTOSAR OSにおける1.保護機能の形式化と2.マルチコア機能におけるハード部分の形式化を行った．
1.保護機能の形式化：AUTOSAR OSのオリジナルの文書では，保護機能の仕様が自然言語(英語)で記述されている．その記述には曖昧な表現が多く，一貫して十分なメモリ保護を規定しているか確信を持つことができない．そこで，まず，形式仕様記述言語Event-Bを用いて，保護機能を形式的に記述した．保護機能の仕様ではread/writeを行う元のコンポーネントと先のコンポーネントの関係に基づいて，read/writeを許可するか，禁止するか規定されている．よって，集合と関係に基づいてOSのコンポーネントの構造を形式化し，その構造に基づいた条件として許可するか禁止するか記述した．これにより，保護機能の記述を明確にすることができ，また，オリジナルの仕様における曖昧な箇所を多数指摘することもできた．
2.マルチコア機能におけるハード部分の形式化：AUTOSAR OSのマルチコア機能における基本的な仕組みであるスピンロックに焦点を当てた．スピンロックを実現するプログラムは小規模であり，アセンブラで数十行である．しかしながら，その実行の際に，複数のコア間で複雑な動作が行われるため，プログラムの正しさを確信することは非常に困難である．プログラムだけでなく，ハード部分の挙動も含めて検証する必要がある．そこで，まず，マルチコアのARMプロセッサにおけるコア間の挙動の形式化を行った．ここでは，プログラムの検証に必要な情報に絞ってモデル化を行い，操作的意味論に基づいて，その挙動を形式的に表現した．これにより，プログラムの実行に伴って，ハード部分で発生する動作を明確にすることができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画では，平成２７年度は，AUTOSAR OS仕様の分析と整理，および，Event-Bによる形式化を実施することを計画していた．研究実績の概要で記述したとおり，実際には，これらに加えて，マルチコア機能におけるハード部分の形式化を行うことができた．この形式モデルは，TOPPERS/ATK2のスピンロックを実現するプログラムを解析しながら作成したものである．また，このモデルを用いて単純なアセンブラプログラムを検証する試みも行った．この試みでは，証明しなければならない条件が大量に生成されたため，検証は完了していないが，解決しなければならない問題は明確になった．平成２８年度は，TOPPERS/ATK2の実装について分析を行い，形式検証を適用する方向性を明らかにする予定であるが，平成２７年度に行った以上の試みにより，ある程度，分析は完了し，検証の方向性は見えてきたと言える．よって，当初の計画以上に進展していると判断した．
|
| Strategy for Future Research Activity |
平成２８年度は，1)AUTOSAR OSの実装の分析，および，2)保護機能の形式検証を行う予定である．
1) AUTOSAR OSの実装の分析：本研究課題では，TOPPERS/ATK2を形式検証の対象とする．そこで，まず，TOPPERS/ATK2の実装について分析を行い，形式検証を適用する方向性を明らかにする．形式検証では，モデル検査と定理証明を用いる予定である．定理証明は，基本的には，述語論理で表現したものが対象であり，プログラムを検証するためには，ホーア論理や検証条件生成などのプログラム検証手法を応用する必要がある．さらに，モデル検査は自動的に検証を行えるが，状態爆発と呼ばれる，規模に関する問題がある．定理証明は，帰納法などにより規模に関する問題は無いが，対話的に検証を行うため，コストが高い．そこで，これらの特性を考慮しながら，事前に適切な技法の選択を行う必要がある．
2) 保護機能の形式検証：2で作成した形式仕様に規定されている保護機能が十分であることを検証する．平成２７年度に作成した形式仕様をEvent-Bのための支援ツールであるRODINを用いて記述する．そして，その記述が一貫していること，および，保護が十分であることを検証する．Event-B/RODINでは，不変表明を記述して，それが常に成立することを定理証明ツールを用いて証明することができる．そこで，作成した形式仕様が一貫していること，および，保護が十分であることを不変表明として記述し，証明を行う．
|
