本研究では，AUTOSAR OSの先進機能を形式検証する手法を提案した．AUTOSAR OSでは，次世代の自動車を見据えて，保護機能とマルチコア機能が提供されている．そこで，これらの機能を実践的に形式検証する手法を提案した．保護機能の形式検証では，AUTOSAR OSの仕様書に基づいて形式仕様を作成し，定理証明による検証過程において，仕様の矛盾を発見することに成功した．マルチコア機能の検証では，複数のメモリモデルに基づいてプログラムを自動定理証明により自動検証する手法を提案し，Linux，TOPPERS/FMP化ネールなどで用いられているspinlockプログラムの形式検証に成功した．