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

2022 年度 実績報告書

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

研究課題

研究課題/領域番号 18H03220
研究機関北陸先端科学技術大学院大学

研究代表者

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

研究分担者 石井 大輔  北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
研究期間 (年度) 2018-04-01 – 2023-03-31
キーワード形式手法 / 車載システム / ハイブリッドシステム / テスト
研究実績の概要

2022年度は,本研究課題の最終年度となる.そこで,これまでの成果を統合し,次世代車載システムのための形式手法としてまとめると共に,評価のための実験を実施した.提案手法は,知能化システムのための手法,ハイブリッドシステムのための手法,メニーコアシステムのための手法により構成される.
1. 知能化システムのための手法.本研究では,これまでに,形式仕様記述言語BBSL(Bounding Box Specification Language),および,BBSLで記述された仕様(BBSL仕様と呼ぶ)に基づくテスト手法を提案した.今年度は,Yolov3を自動運転システムの画像認識部分に利用することを想定した実験を実施した.実験では,いくらかの非安全な誤認識が発生することを検出することができた.これにより,提案手法が,実践的な自動運転システムにおいて有効に働くことを確認できた.
2. ハイブリッドシステムのための手法.本研究では,これまでに,乱択に基づいた手法を提案し,その後,SMTソルバに基づいた手法を提案してきた.2022年度は,これらを併用する手法を提案した.また,実践的なMATLAB/Simulinkモデルを用いた実験を実施し,個々の手法,および,競合ツールであるSLDV(Simulink Design Verifier)に勝ることを確認することができた.
3. メニーコアシステムのための手法.本研究では,これまでに,汎用プログラミング言語Rustを用いたメニーコアOSのテストケース自動生成手法を提案した.本年度は,POSIX準拠のLinuxを対象とした実験を実施し,提案手法の評価を行った.これにより,メニーコアOSの仕様と実装の間に多くの乖離があることが検出でき,提案手法の有効性を確認できた.

現在までの達成度 (段落)

令和4年度が最終年度であるため、記入しない。

今後の研究の推進方策

令和4年度が最終年度であるため、記入しない。

  • 研究成果

    (8件)

すべて 2022

すべて 雑誌論文 (2件) (うち査読あり 2件、 オープンアクセス 2件) 学会発表 (6件) (うち国際学会 5件)

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

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

      Software Testing, Verification and Reliability

      巻: 32 ページ: -

    • DOI

      10.1002/stvr.1828

    • 査読あり / オープンアクセス
  • [雑誌論文] 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

    • 査読あり / オープンアクセス
  • [学会発表] 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
    • 国際学会
  • [学会発表] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • 学会等名
      NASA Formal Methods
    • 国際学会
  • [学会発表] 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
    • 国際学会
  • [学会発表] 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
    • 国際学会
  • [学会発表] 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

    • 著者名/発表者名
      青木利晃,冨田尭,河井達治,川上大介,千田伸男
    • 学会等名
      ソフトウェアエンジニアリングシンポジウム

URL: 

公開日: 2023-12-25  

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

Powered by NII kakenhi