| 研究実績の概要 |
平成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における先進機能の実践的な形式検証手法を提案できたと言える．
|
