次世代車載オペレーティングシステムにおける先進機能の形式検証に関する研究

• 資料種別: 文書・図像類
• タイトル: 次世代車載オペレーティングシステムにおける先進機能の形式検証に関する研究
• 著者・編者: 青木, 利晃
• 著者標目: 青木, 利晃
• 出版年月日等: 2018-05-15
• 出版年（W3CDTF）: 2018-05-15
• 並列タイトル等: Formal verification of advanced functionalities in next-generation automotive operating systems
• タイトル（掲載誌）: 科学研究費助成事業研究成果報告書
• 掲載ページ: 1-5
• 本文の言語コード: jpn
• 件名標目: 形式手法; 形式検証; 車載システム; 形式仕様; 定理証明
• 対象利用者: 一般
• 一般注記: 本研究では，AUTOSAR OSの先進機能を形式検証する手法を提案した．AUTOSAR OSでは，次世代の自動車を見据えて，保護機能とマルチコア機能が提供されている．そこで，これらの機能を実践的に形式検証する手法を提案した．保護機能の形式検証では，AUTOSAR OSの仕様書に基づいて形式仕様を作成し，定理証明による検証過程において，仕様の矛盾を発見することに成功した．マルチコア機能の検証では，複数のメモリモデルに基づいてプログラムを自動定理証明により自動検証する手法を提案し，Linux，TOPPERS/FMP化ネールなどで用いられているspinlockプログラムの形式検証に成功した．：We proposed methods to formally verify advanced functions of AUTOSAR operating system. Protection function and multicore function are provided for next generation cars in AUTOSAR operating system. Thus, we proposed practical methods to formally verify those functions. In the formal verification of the protection function, its formal specification was developed based on the specification of AUTOSAR operating system and we succeeded in finding the inconsistency of the AUTOSAR operating system specification during proving the consistency of the specification by theorem proving. In the formal verification of the multicore function, we proposed a method to automatically verify programs by automated theorem proving based on multiple memory models, and successfully verified spinlock programs of real operating systems such as Linux and TOPPERS/FMP.; 基盤研究(C)（一般）; 研究期間：2015～2017; 課題番号：15K00094; 研究者番号：20313702; 研究分野：ソフトウェア工学; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/15390
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ