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

• 研究課題/領域番号: 15K00094
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウェア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 青木 利晃 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)
• 研究期間 (年度): 2015-04-01 – 2018-03-31
• 研究課題ステータス: 完了 (2017年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2017年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2016年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2015年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 形式手法 / 形式検証 / 車載システム / 形式仕様 / 定理証明

研究成果の概要

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

研究成果

• [雑誌論文] A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX (2016)
  • 著者名/発表者名: Min Zhang, Toshiaki Aoki, Yueying He
  • 雑誌名: Journal of Information Security and Applications 巻: 31 ページ: 41-53
  • DOI: 10.1016/j.jisa.2016.05.002
  • 査読あり / オープンアクセス / 国際共著
• [雑誌論文] A Framework for Verifying the Conformance of Design to Its Formal Specifications (2015)
  • 著者名/発表者名: Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E98.D 号: 6 ページ: 1137-1149
  • DOI: 10.1587/transinf.2014FOP0004
  • NAID: 130005072395
  • ISSN: 0916-8532, 1745-1361
  • 査読あり
• [雑誌論文] Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach (2015)
  • 著者名/発表者名: Haitao Zhang, Toshiaki Aoki, Yuki Chiba
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E98.D 号: 10 ページ: 1765-1776
  • DOI: 10.1587/transinf.2015EDP7043
  • NAID: 130005101306
  • ISSN: 0916-8532, 1745-1361
  • 査読あり
• [学会発表] Domain-Specific Language Facilitates Scheduling in Model Checking (2017)
  • 著者名/発表者名: Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki
  • 学会等名: Asia-Pacific Software Engineering Conference
  • 国際学会
• [学会発表] A Reusable Framework for Modeling and Verifying In-vehicle Networking System in the Presence of CAN and FlexRay (2017)
  • 著者名/発表者名: Xiaoyun Guo, Hsin-Hung Lin, Toshiaki Aoki, Yuki Chiba
  • 学会等名: Asia-Pacific Software Engineering Conference
  • 国際学会
• [学会発表] Template-Based Monte-Carlo Test Generation for Simulink Models, Seventh Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (2017)
  • 著者名/発表者名: Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
  • 学会等名: Workshop on Design, Modeling and Evaluation of Cyber Physical Systems
  • 国際学会
• [学会発表] Assembly Program Verification for Multiprocessors with Relaxed Memory Model using SMT Solver (2017)
  • 著者名/発表者名: Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki
  • 学会等名: International Symposium on Theoretical Aspects of Software Engineering
  • 国際学会
• [学会発表] Simulinkモデルに対するテストスイート自動生成 (2016)
  • 著者名/発表者名: 冨田尭, 石井大輔，青木利晃
  • 学会等名: 第14回ディペンダブルシステムワークショップ
  • 発表場所: 花びしホテル(北海道函館市)
  • 年月日: 2016-12-14
• [学会発表] Java Pathfinder における弱公平性条件の実装 (2016)
  • 著者名/発表者名: 太田十字光, 田辺良則, 青木利晃
  • 学会等名: 日本ソフトウェア科学会第33回全国大会
  • 発表場所: 東北大学片平キャンパス(宮城県仙台市)
  • 年月日: 2016-09-06
• [学会発表] Verifying OSEK/VDX OS Design using Its Formal Specification (2016)
  • 著者名/発表者名: Dieu Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
  • 学会等名: International Symposium on Theoretical Aspects of Software Engineering
  • 発表場所: Shanghai, China
  • 年月日: 2016-07-17
  • 国際学会
• [学会発表] Dissolution of the Gap between Safety Requirements Written in a Natural Language and Formal Notations (2016)
  • 著者名/発表者名: Masahiro Matsubara, Fumio Narisawa, Atsuhiro Ohno, Toshiaki Aoki, Yuki Chiba
  • 学会等名: SAE 2016 World Congress and Exhibition
  • 発表場所: Detroit, USA
  • 年月日: 2016-04-12
  • 国際学会
• [学会発表] ISO26262のための安全要求記述言語と追跡可能性検証手法の提案 (2016)
  • 著者名/発表者名: 青木利晃，千葉勇輝，松原正裕，成沢文雄
  • 学会等名: プログラミングおよびプログラミング言語ワークショッ プ
  • 発表場所: ダイヤモンド瀬戸内マリンホテル(岡山県たまの市)
  • 年月日: 2016-03-07
• [学会発表] Modeling Safety Requirements of ISO26262 using Goal Trees and Patterns (2015)
  • 著者名/発表者名: Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi, Fumio Narisawa
  • 学会等名: International Workshop on Formal Techniques for Safety-Critical Systems
  • 発表場所: Paris, France
  • 年月日: 2015-11-06
  • 国際学会
• [学会発表] ゴール木とパターンを用いたISO26262における安全要求のモデル化 (2015)
  • 著者名/発表者名: 青木利晃，トライチャイヤポーンクリアンクライ，千葉勇輝，松原正裕，西昌能，成沢文雄
  • 学会等名: 組込みシステムシンポジウム
  • 発表場所: 早稲田大学グリーン・コンピューティング・システム研究開発センター(東京都新宿区)
  • 年月日: 2015-10-21
• [学会発表] Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking (2015)
  • 著者名/発表者名: Hideto Ogawa, Makoto Ichii, Fumihiro Kumeno, Toshiaki Aoki
  • 学会等名: COMPSAC2015
  • 発表場所: Taichung, Taiwan
  • 年月日: 2015-07-01
  • 国際学会
• [学会発表] Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications (2015)
  • 著者名/発表者名: Haitao Zhang, Toshiaki Aoki, Yuki Chiba
  • 学会等名: IEEE International Conference on Software Testing, Verification and Validation
  • 発表場所: Graz, Austria
  • 年月日: 2015-04-13
  • 国際学会
• [図書] Cyber-Physical System Design from an Architecture Analysis Viewpoint (2017)
  • 著者名/発表者名: Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake, Tomoji Kishi
  • 総ページ数: 159
  • 出版者: Springer
  • ISBN: 9789811044366