次世代車載基盤システムのための
形式手法と
検証ツールの創出
SCROLL
RESEARCH 研究概要
本研究では、次世代車載基盤システムの安全性・信頼性を保証する形式手法および検証ツールを提案する。提案手法は次世代車載基盤システムの認識から制御までをカバーし、形式仕様言語、制御仕様言語、そして、それらを用いた形式検証手法で構成する。提案手法において自動化可能な部分を検証ツールとして実現する。提案手法および検証ツールは、自動運転に関するオープンデータの利用、および、自動運転実証実験グループとの連携により評価する。本研究の成果により、自動運転を支える基盤の安全性と信頼性が飛躍的に向上し、安全安心なモビリティ社会の実現が期待される。
研究終了時の達成目標
産業応用できる形式手法の提案だけでなく、ツールをリリースし、それらの有効性が、オープンデータや自動運転実証実験により定量的に示されていること。
研究の独創性、新規性・優位性
国内外において、自動運転の実証実験は多く実施されているが、自動運転に特化した制御理論やサービスの実証に関するものがほとんどである。車載システムを想定して、電子制御システムの形式検証を行う試みは数多く存在する。しかしながら、ほとんどの研究は単純化された例やシステムの一部にしか適用されていない。本研究のように、形式手法により、自動運転を支える車載基盤システムの仕様記述から制御システムまでの統合的な安全性・信頼性検証手法を提案するものは見受けられない。本研究の優位性は、科学的アプローチである形式手法の実践にこだわっていることである。形式手法により自動運転システムの安全性・信頼性を統合的に検証した実績は、まだ報告されておらず、世界初の事例となることが期待される。
研究の将来展望
1.CREST研究期間終了後の研究計画
本研究では、提案手法を支援・実現するツールを実装する。オープンデータ、および、自動運転実証実験との連携により獲得した、提案手法の有効性を示したデータを公開する予定である。これらに基づき、研究期間終了後、提案手法の普及や実製品への適用などの活動を行う。
2.科学技術イノベーション※
本研究で提案するツールは、オープンソース、および、商用ツールとして、産業界に還元する。これにより、次世代の自動車の安全性・信頼性が飛躍的に向上することが期待される。
※創出、 知的財産権の取得・活用、新産業創出・社会貢献