| 研究課題/領域番号 |
15K00094
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
青木 利晃 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 車載システム / 形式仕様 / 形式検証 |
|---|
| 研究実績の概要 |
平成28年度は，1.AUTOSAR OSの保護機能の形式検証，および，2.マルチコア機能の形式検証を実施した．
1.AUTOSAR OSの保護機能の形式検証：平成27年度は，Event-Bを用いてAUTOSAR OSの保護機能を形式的に記述した．Event-Bでは，証明課題(proof obligation)と呼ばれる証明しなければならない事実を自動生成する．この証明課題はEvent-BのツールRODINの証明器を用いて対話的に証明を行う．平成27年度において，証明課題の証明を試みたが，それら全部は証明することができなかった．そこで，今年度も，証明を引き続き行ったが，RODINの証明器の信頼性や機能の問題により，それらすべてについて証明を行うことが困難になった．そこで，AlloyとAlloy Analyzerを用いて自動的に証明を行うことにした．Alloyは集合や関係に基づいた仕様を記述するための言語であり，Alloy Analyzerはその検証ツールである．これらは，Event-Bで記述したものと同等のものを扱うことができる．今年度はAlloyで保護機能を記述し，Alloy Analyzerを用いて自動検証を実施することができた．
2.マルチコア機能の形式検証：マルチコアプロセッサ上で動作するプログラムでは，複数のコア間でハードウェアレベルの複雑な動作が実行されるため，検証対象のプログラムだけでなく，ハードウェアの振る舞いを含めて検証する必要がある．そこで，平成27年度に，ハードウェアの振る舞いの分析と形式化を行った．そして，今年度は，その分析と形式化に基づいたプログラムの検証法を提案した．この手法では，自動定理証明器(SMTソルバ)を用いて検証を行う．また，提案手法を，Linuxカーネルにおけるスピンロックのプログラムに適用し，実際に検証を行うことができた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
今年度は，1.保護機能の形式検証と2.マルチコア機能の形式検証を行った．1については，当初の予定どおり，形式検証を実施することができたため，おおむね予定どおりに進展していると考えている．2については，以下の理由から，当初の計画以上に進展していると考えている．当初の計画では，今年度は，AUTOSAR OSの実装の分析を行う予定であった．しかしながら，その大半は，昨年度実施することができ，今年度は，マルチコア機能の形式検証の仕組みについて提案することができた．この手法では，自動定理証明器(SMTソルバ)を用いて，自動的に検証を行うことができる．当初は，定理証明による対話的な証明を想定していたが，自動的な検証が可能になったことは，大きな成果である．さらに，提案手法により，SPARC用のLinuxカーネルにおけるスピンロックプログラムの検証に成功し，また，すでにバグがあることがわかっているプログラム(このプログラムは当該分野のベンチマークのように使われている)の検証を実施し，バグを検出することにも成功した．すでに，実践的に使える手法を提案することができたのである．これらのことから，当初の計画以上に進展していると判断した．
|
| 今後の研究の推進方策 |
平成29年度は，実際の車載OSを対象として，1.保護機能の検証，および，2.マルチコア機能の検証を実施し，提案手法の評価を行う．
1.保護機能の検証:平成28年度に，Alloyによる保護機能の形式仕様を作成し，その正しさの検証を実施した．平成29年度は，この形式仕様に基づいて，車載OSの検証を行う手法を提案する．この検証では，形式仕様から網羅的なテストケースおよび期待値を自動生成し，それらを用いたテストを実施することを考えている．ここで，保護機能の仕様は，静的な制約として規定されており，形式仕様も同様である．テストケースを自動生成するためには，車載OSを実行する手順を規定する情報が必要である．そこで，テストする手順を規定するモデルを追加し，形式仕様からテストケースを自動生成する手法を提案する予定である．
2.マルチコア機能の検証
平成28年度に，すでに，SPARC用のLinuxカーネルの検証には成功している．一方，対象とする車載OSはARMプロセッサを用いているが，その挙動はSPARCとは異なる．SPARCはTSOと呼ばれるメモリモデルを採用しているが，ARMプロセッサは，それとは異なるメモリモデルを採用しているためである．そこで，提案手法をARMプロセッサが扱えるように拡張し，検証を実施する．
|
