• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

次世代車載システムのための形式手法に関する研究

研究課題

研究課題/領域番号 18H03220
研究種目

基盤研究(B)

配分区分補助金
応募区分一般
審査区分 小区分60050:ソフトウェア関連
研究機関北陸先端科学技術大学院大学

研究代表者

青木 利晃  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)

研究分担者 石井 大輔  北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
研究期間 (年度) 2018-04-01 – 2023-03-31
研究課題ステータス 完了 (2022年度)
配分額 *注記
17,030千円 (直接経費: 13,100千円、間接経費: 3,930千円)
2022年度: 3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2021年度: 2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2020年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円)
2019年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円)
2018年度: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
キーワード形式手法 / 形式検証 / 形式仕様記述 / 車載システム / ハイブリッドシステム / モデル検査 / 充足可能性判定 / テスト / 不確定性
研究成果の概要

本研究では,次世代車載システムを対象として,それらの高信頼性と高安全性を実現する形式手法を提案した.次世代車載システムでは,知能化システムに由来する不確実性,画像や動画を含む多様で大量のデータの取扱,高度な制御に由来する計算の複雑さに関する問題がある.本研究では,従来の形式手法を拡張・特化した手法,および,新規の形式手法を提案し,これらの問題を解決・緩和した.実践的な手法となるよう別手法との組み合わせた解決策も提案した.提案手法は,オープンデータセットや公開文書を用いて評価した.成果の一部は,商用ツールとしてリリースすることにも成功した.これらのことから,実践的な手法が提案できたと言える.

研究成果の学術的意義や社会的意義

形式手法は,一筋縄では実践が行えないため,実践のための理論や技術も学術的な研究の対象である.本研究では,形式手法を用いた複数の実践例を示すことができ,次世代車載システムのような先進システムにおいても形式手法が有効であることを示すことがでた.これは,当該分野の発展に大きく貢献すると考えている.また,本研究では,提案手法に基づいたツールを実装し,商用ツール,および,オープンソースとしてリリースした.これらは,産業界に直接的に還元できるものである.本研究の成果が普及することにより,自動車に限らず,同様の先進システムの信頼性・安全性が格段に高くなり,安全・安心な社会構築へ貢献することが期待される.

報告書

(6件)
  • 2022 実績報告書   研究成果報告書 ( PDF )
  • 2021 実績報告書
  • 2020 実績報告書
  • 2019 実績報告書
  • 2018 実績報告書
  • 研究成果

    (39件)

すべて 2022 2021 2020 2019 2018

すべて 雑誌論文 (10件) (うち国際共著 2件、 査読あり 10件、 オープンアクセス 8件) 学会発表 (29件) (うち国際学会 22件、 招待講演 3件)

  • [雑誌論文] Comprehensive evaluation of file systems robustness with SPIN model checking2022

    • 著者名/発表者名
      Yuan Jingcheng、Aoki Toshiaki、Guo Xiaoyun
    • 雑誌名

      Software Testing, Verification and Reliability

      巻: 32 号: 6

    • DOI

      10.1002/stvr.1828

    • 関連する報告書
      2022 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Compliance SSI System Property Set to Laws, Regulations, and Technical Standards2022

    • 著者名/発表者名
      Pattiyanon Charnon、Aoki Toshiaki
    • 雑誌名

      IEEE Access

      巻: 10 ページ: 99370-99393

    • DOI

      10.1109/access.2022.3204112

    • 関連する報告書
      2022 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Integrating Pattern Matching and Abstract Interpretation for Verifying Cautions Microcontrollers2021

    • 著者名/発表者名
      Thuy Nguyen, Takashi Tomita, Junpei Endo, Toshiaki Aoki
    • 雑誌名

      Journal of Software: Testing, Verification and Reliability

      巻: 31(8) 号: 8

    • DOI

      10.1002/stvr.1788

    • 関連する報告書
      2021 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models2020

    • 著者名/発表者名
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • 雑誌名

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      巻: E103.A 号: 2 ページ: 451-461

    • DOI

      10.1587/transfun.2019MAP0010

    • NAID

      130007793381

    • ISSN
      0916-8508, 1745-1337
    • 年月日
      2020-02-01
    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] A framework for assume-guarantee regression verification of evolving software2020

    • 著者名/発表者名
      Hoang Viet Tran, Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki
    • 雑誌名

      Science of Computer Programming

      巻: 193

    • 関連する報告書
      2020 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Multiple conformance to hybrid-automata-modelled requirements for detecting indoor temperature anomalies2020

    • 著者名/発表者名
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • 雑誌名

      Indoor and Built Environment

      巻: - 号: 9 ページ: 1441-1465

    • DOI

      10.1177/1420326x20941576

    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Model checking of in-vehicle networking systems with CAN and FlexRay2020

    • 著者名/発表者名
      Guo Xiaoyun、Aoki Toshiaki、Lin Hsin-Hung
    • 雑誌名

      Journal of Systems and Software

      巻: 161 ページ: 110461-110461

    • DOI

      10.1016/j.jss.2019.110461

    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies2019

    • 著者名/発表者名
      TRAN Nhat-Hoa、CHIBA Yuki、AOKI Toshiaki
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E102.D 号: 7 ページ: 1280-1295

    • DOI

      10.1587/transinf.2017EDP7391

    • NAID

      130007671332

    • ISSN
      0916-8532, 1745-1361
    • 年月日
      2019-07-01
    • 関連する報告書
      2019 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver2018

    • 著者名/発表者名
      MALEEHUAN Pattaravut、CHIBA Yuki、AOKI Toshiaki
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E101.D 号: 12 ページ: 3038-3058

    • DOI

      10.1587/transinf.2018EDP7099

    • NAID

      130007539295

    • ISSN
      0916-8532, 1745-1361
    • 年月日
      2018-12-01
    • 関連する報告書
      2018 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] 車載システム開発における形式手法実践の現状と課題2018

    • 著者名/発表者名
      青木 利晃
    • 雑誌名

      システム/制御/情報

      巻: 62 号: 4 ページ: 134-140

    • DOI

      10.11509/isciesci.62.4_134

    • NAID

      130007498124

    • ISSN
      0916-1600, 2424-1806
    • 年月日
      2018-04-15
    • 関連する報告書
      2018 実績報告書
    • 査読あり / オープンアクセス
  • [学会発表] A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems2022

    • 著者名/発表者名
      Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida
    • 学会等名
      COMPSAC
    • 関連する報告書
      2022 実績報告書
    • 国際学会
  • [学会発表] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • 学会等名
      NASA Formal Methods
    • 関連する報告書
      2022 実績報告書
    • 国際学会
  • [学会発表] Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques2022

    • 著者名/発表者名
      Thuy Nguyen, Takashi Tomita, Junpei Endo, Geon-ung Kang, Toshiaki Aoki
    • 学会等名
      Symposium On Applied Computing
    • 関連する報告書
      2022 実績報告書
    • 国際学会
  • [学会発表] SMT-Based Model Checking of Industrial Simulink Models2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
    • 学会等名
      International Conference on Formal Engineering Method
    • 関連する報告書
      2022 実績報告書
    • 国際学会
  • [学会発表] Coverage Testing of Industrial Simulink Models Using Monte-Carlo and SMT-Based Methods2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do and Hideaki Takai
    • 学会等名
      International Conference on Software Quality, Reliability, and Security
    • 関連する報告書
      2022 実績報告書
    • 国際学会
  • [学会発表] 自動運転システムを対象としたシナリオ開発のためのモデリング言語2022

    • 著者名/発表者名
      青木利晃,冨田尭,河井達治,川上大介,千田伸男
    • 学会等名
      ソフトウェアエンジニアリングシンポジウム
    • 関連する報告書
      2022 実績報告書
  • [学会発表] Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations2022

    • 著者名/発表者名
      Charnon Pattiyanon, Toshiaki Aoki
    • 学会等名
      8th International Conference on Information Systems Security and Privacy (ICISSP)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations2022

    • 著者名/発表者名
      Charnon Pattiyanon, Toshiaki Aoki, Daisuke Ishii
    • 学会等名
      8th International Conference on Information Systems Security and Privacy (ICISSP)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] SSpinJa: Facilitating Schedulers in Model Checking2021

    • 著者名/発表者名
      Nhat-Hoa Tran, Toshiaki Aoki
    • 学会等名
      21th IEEE International Conference on Software Quality, Reliability, and Security(QRS)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] 自動運転システム開発におけるシミュレーション検証のためのテストケース作成手法の提案2021

    • 著者名/発表者名
      鈴木玄貴,冨田尭,青木利晃,河井達治,川上大介,千田伸男
    • 学会等名
      情報処理学会 第207回ソフトウェア工学研究発表会
    • 関連する報告書
      2020 実績報告書
  • [学会発表] Comprehensive Robustness Evaluation of File Systems with Model Checking2020

    • 著者名/発表者名
      Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo
    • 学会等名
      International Conference on Software Quality, Reliability, and Security
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Risk Assessment Using Coloured Petri Nets for Telemedicine2020

    • 著者名/発表者名
      Kenji Fujita, Kunihiko Hiraishi, Toshiaki Aoki
    • 学会等名
      International Conference on Industrial Engineering and Engineering Management
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems2020

    • 著者名/発表者名
      Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita
    • 学会等名
      IEEE Pacific Rim International Symposium on Dependable Computing
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] 自動運転システムにおける画像を対象とした形式仕様記述言語BBSLの提案2020

    • 著者名/発表者名
      田中健人,青木利晃,川上大介,千田伸男,河井達治,冨田尭
    • 学会等名
      情報処理学会 第205回ソフトウェア工学研究発表会
    • 関連する報告書
      2020 実績報告書
  • [学会発表] A Scalable Monte-Carlo Test-Case Generation Tool for Large and Complex Simulink Models2019

    • 著者名/発表者名
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • 学会等名
      11th Workshop on Modelling in Software Engineering
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Reducing False Positives of Static Analysis for SEI CERT C Coding Standard2019

    • 著者名/発表者名
      Thu Trang Nguyen, Pattaravut Maleehuan, Toshiaki Aoki, Takashi Tomita, Iori Yamada
    • 学会等名
      Joint International Workshop on Conducting Empirical Studies in Industry and 6th International Workshop on Software Engineering Research and Industrial Practice
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Compaction of Spacecraft Operation Model using Domain Knowledge based Stereotype2019

    • 著者名/発表者名
      Kazunori Someya, Naoki Ishihama, Keiichi Wada, Toshiaki Aoki
    • 学会等名
      International Symposium on Space Technology and Science
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Conformance Testing of Schedulers for DSL-based Model Checking2019

    • 著者名/発表者名
      Nhat-Hoa Tran and Toshiaki Aoki
    • 学会等名
      26th International SPIN Symposium on Model Checking of Software
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard2019

    • 著者名/発表者名
      Thu-Trang Nguyen, Toshiaki Aoki, Takashi Tomita and Iori Yamada
    • 学会等名
      Asia-Pacific Software Engineering Conference
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller2019

    • 著者名/発表者名
      Thuy Nguyen, Toshiaki Aoki, Takashi Tomita and Junpei Endo
    • 学会等名
      Asia-Pacific Software Engineering Conference
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Model Checking Automotive Systems2019

    • 著者名/発表者名
      Toshiaki Aoki
    • 学会等名
      Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things
    • 関連する報告書
      2019 実績報告書
    • 国際学会 / 招待講演
  • [学会発表] Event-Bに基づいた鉄道システムの実践的な形式化と検証2019

    • 著者名/発表者名
      太田十字光, 青木利晃
    • 学会等名
      情報処理学会 第203回ソフトウェア工学研究会
    • 関連する報告書
      2019 実績報告書
  • [学会発表] Qualitative and Quantitative Analysis with Scheduling Policies in Model Checking2018

    • 著者名/発表者名
      Nhat-Hoa Tran, Yuki Chiba and Toshiaki Aoki
    • 学会等名
      The 33rd ACM/SIGAPP Symposium On Applied Computing
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] Formalization and Verification of AUTOSAR OS Standard's Memory Protection2018

    • 著者名/発表者名
      Trinh Le Khanh, Yuki Chiba and Toshiaki Aoki
    • 学会等名
      The 12th International Symposium on Theoretical Aspects of Software Engineering
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change2018

    • 著者名/発表者名
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • 学会等名
      IEEE/ACM the 22nd International Symposium on Distributed Simulation and Real Time Applications
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems2018

    • 著者名/発表者名
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • 学会等名
      The 23rd IEEE Pacific Rim International Symposium on Dependable Computing
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] 確率統計に基づいた故障木とテストによる機械学習システムの系統的評価手法2018

    • 著者名/発表者名
      青木利晃,川上大介,千田伸男,冨田尭
    • 学会等名
      ソフトウェアエンジニアリングシンポジウム
    • 関連する報告書
      2018 実績報告書
  • [学会発表] 形式手法と安全性2018

    • 著者名/発表者名
      青木利晃
    • 学会等名
      安全工学会 安全工学研究発表会
    • 関連する報告書
      2018 実績報告書
    • 招待講演
  • [学会発表] 車載システム開発における形式手法実践の現状と課題2018

    • 著者名/発表者名
      青木利晃
    • 学会等名
      日本ソフトウェア科学会 第16回 ディペンダブルシステムワークショップ
    • 関連する報告書
      2018 実績報告書
    • 招待講演

URL: 

公開日: 2018-04-23   更新日: 2024-01-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi