研究実績の概要 |
平成29年度は,これまで提案してきた検証手法を,1.AUTOSAR OSの保護機能,および,2.マルチコア機能に適用し,評価を行った. 1. AUTOSAR OSの保護機能の検証. 本研究では,昨年度までにAlloyによりAUTOSAR OSの保護機能の形式仕様を作成した.しかしながら,Alloyでは,特定の場合についての妥当性確認は可能であるが,任意の場合についての無矛盾性を保証できない.Alloyでは,定理証明を行うことができないためである.そこで,定理証明が可能であるEvent-Bにより形式仕様を作成した.Event-Bでは,不変表明に基づいて証明責務と呼ばれる条件が生成され,これらを証明することにより,不変表明が成立することを保証する.本研究では,保護機能の無矛盾性を保証する不変表明を記述し,証明責務の証明を行った.ここで,証明できない証明責務が存在したため,分析したところ,オリジナルの仕様の矛盾を発見した.そして,その仕様を修正することにより,無矛盾性を証明することができた. 2.マルチコア機能の検証.昨年度までに提案した自動定理証明器(SMTソルバ)を用いた自動検証手法をARMプロセッサベースの車載OSであるTOPPERS/FMPカーネルのスピンロック機能の検証に適用した.この検証では,SC, TSO, ARMのメモリモデルで検証を実施して,これらすべてのメモリモデルに対して,スピンロック機能が正しく動作することを確認できた. 以上のように,本研究では,最終的に,実際のAUTOSAR OSの仕様,および,AUTOSAR OSの実装を検証することに成功した.さらに,仕様の検証では,矛盾を指摘することができた.これらのことから,車載OSにおける先進機能の実践的な形式検証手法を提案できたと言える.
|