• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Study on formal methods for next-generation automotive systems

Research Project

Project/Area Number 18H03220
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Review Section Basic Section 60050:Software-related
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

Aoki Toshiaki  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (20313702)

Co-Investigator(Kenkyū-buntansha) 石井 大輔  北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
Project Period (FY) 2018-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥17,030,000 (Direct Cost: ¥13,100,000、Indirect Cost: ¥3,930,000)
Fiscal Year 2022: ¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2021: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2020: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2019: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2018: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Keywords形式手法 / 形式検証 / 形式仕様記述 / 車載システム / ハイブリッドシステム / モデル検査 / 充足可能性判定 / テスト / 不確定性
Outline of Final Research Achievements

In this research, we proposed a formal method and a verification method for next-generation automotive systems to achieve their high reliability and high safety. The next-generation automotive systems face problems regarding uncertainty coming from intelligent systems, handling of a large amount of diverse data including images and videos, and computational complexity arising from advanced control. In this research, we proposed an extended and specialized version of conventional formal methods as well as new formal methods to solve and mitigate these problems. We also proposed solutions in combination with the other methods such as testing, modeling, and simulation to make our formal methods practical. We demonstrated the effectiveness of our method using open datasets and public documents. In addition, some of the research results have been successfully released as a commercial tool. Thus, we can say that we succeeded in proposing a practical method.

Academic Significance and Societal Importance of the Research Achievements

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

Report

(6 results)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • 2018 Annual Research Report
  • Research Products

    (39 results)

All 2022 2021 2020 2019 2018

All Journal Article (10 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 10 results,  Open Access: 8 results) Presentation (29 results) (of which Int'l Joint Research: 22 results,  Invited: 3 results)

  • [Journal Article] Comprehensive evaluation of file systems robustness with SPIN model checking2022

    • Author(s)
      Yuan Jingcheng、Aoki Toshiaki、Guo Xiaoyun
    • Journal Title

      Software Testing, Verification and Reliability

      Volume: 32 Issue: 6

    • DOI

      10.1002/stvr.1828

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Compliance SSI System Property Set to Laws, Regulations, and Technical Standards2022

    • Author(s)
      Pattiyanon Charnon、Aoki Toshiaki
    • Journal Title

      IEEE Access

      Volume: 10 Pages: 99370-99393

    • DOI

      10.1109/access.2022.3204112

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Integrating Pattern Matching and Abstract Interpretation for Verifying Cautions Microcontrollers2021

    • Author(s)
      Thuy Nguyen, Takashi Tomita, Junpei Endo, Toshiaki Aoki
    • Journal Title

      Journal of Software: Testing, Verification and Reliability

      Volume: 31(8) Issue: 8

    • DOI

      10.1002/stvr.1788

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models2020

    • Author(s)
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • Journal Title

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      Volume: E103.A Issue: 2 Pages: 451-461

    • DOI

      10.1587/transfun.2019MAP0010

    • NAID

      130007793381

    • ISSN
      0916-8508, 1745-1337
    • Year and Date
      2020-02-01
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A framework for assume-guarantee regression verification of evolving software2020

    • Author(s)
      Hoang Viet Tran, Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki
    • Journal Title

      Science of Computer Programming

      Volume: 193

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Multiple conformance to hybrid-automata-modelled requirements for detecting indoor temperature anomalies2020

    • Author(s)
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • Journal Title

      Indoor and Built Environment

      Volume: - Issue: 9 Pages: 1441-1465

    • DOI

      10.1177/1420326x20941576

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Model checking of in-vehicle networking systems with CAN and FlexRay2020

    • Author(s)
      Guo Xiaoyun、Aoki Toshiaki、Lin Hsin-Hung
    • Journal Title

      Journal of Systems and Software

      Volume: 161 Pages: 110461-110461

    • DOI

      10.1016/j.jss.2019.110461

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies2019

    • Author(s)
      TRAN Nhat-Hoa、CHIBA Yuki、AOKI Toshiaki
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E102.D Issue: 7 Pages: 1280-1295

    • DOI

      10.1587/transinf.2017EDP7391

    • NAID

      130007671332

    • ISSN
      0916-8532, 1745-1361
    • Year and Date
      2019-07-01
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver2018

    • Author(s)
      MALEEHUAN Pattaravut、CHIBA Yuki、AOKI Toshiaki
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E101.D Issue: 12 Pages: 3038-3058

    • DOI

      10.1587/transinf.2018EDP7099

    • NAID

      130007539295

    • ISSN
      0916-8532, 1745-1361
    • Year and Date
      2018-12-01
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Practical Applications of Formal Methods to Automotive Systems-Current and Future Directions2018

    • Author(s)
      青木 利晃
    • Journal Title

      SYSTEMS, CONTROL AND INFORMATION

      Volume: 62 Issue: 4 Pages: 134-140

    • DOI

      10.11509/isciesci.62.4_134

    • NAID

      130007498124

    • ISSN
      0916-1600, 2424-1806
    • Year and Date
      2018-04-15
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Presentation] A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems2022

    • Author(s)
      Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida
    • Organizer
      COMPSAC
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • Organizer
      NASA Formal Methods
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques2022

    • Author(s)
      Thuy Nguyen, Takashi Tomita, Junpei Endo, Geon-ung Kang, Toshiaki Aoki
    • Organizer
      Symposium On Applied Computing
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] SMT-Based Model Checking of Industrial Simulink Models2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
    • Organizer
      International Conference on Formal Engineering Method
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Coverage Testing of Industrial Simulink Models Using Monte-Carlo and SMT-Based Methods2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do and Hideaki Takai
    • Organizer
      International Conference on Software Quality, Reliability, and Security
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 自動運転システムを対象としたシナリオ開発のためのモデリング言語2022

    • Author(s)
      青木利晃,冨田尭,河井達治,川上大介,千田伸男
    • Organizer
      ソフトウェアエンジニアリングシンポジウム
    • Related Report
      2022 Annual Research Report
  • [Presentation] Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations2022

    • Author(s)
      Charnon Pattiyanon, Toshiaki Aoki
    • Organizer
      8th International Conference on Information Systems Security and Privacy (ICISSP)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations2022

    • Author(s)
      Charnon Pattiyanon, Toshiaki Aoki, Daisuke Ishii
    • Organizer
      8th International Conference on Information Systems Security and Privacy (ICISSP)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] SSpinJa: Facilitating Schedulers in Model Checking2021

    • Author(s)
      Nhat-Hoa Tran, Toshiaki Aoki
    • Organizer
      21th IEEE International Conference on Software Quality, Reliability, and Security(QRS)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 自動運転システム開発におけるシミュレーション検証のためのテストケース作成手法の提案2021

    • Author(s)
      鈴木玄貴,冨田尭,青木利晃,河井達治,川上大介,千田伸男
    • Organizer
      情報処理学会 第207回ソフトウェア工学研究発表会
    • Related Report
      2020 Annual Research Report
  • [Presentation] Comprehensive Robustness Evaluation of File Systems with Model Checking2020

    • Author(s)
      Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo
    • Organizer
      International Conference on Software Quality, Reliability, and Security
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Risk Assessment Using Coloured Petri Nets for Telemedicine2020

    • Author(s)
      Kenji Fujita, Kunihiko Hiraishi, Toshiaki Aoki
    • Organizer
      International Conference on Industrial Engineering and Engineering Management
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems2020

    • Author(s)
      Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita
    • Organizer
      IEEE Pacific Rim International Symposium on Dependable Computing
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 自動運転システムにおける画像を対象とした形式仕様記述言語BBSLの提案2020

    • Author(s)
      田中健人,青木利晃,川上大介,千田伸男,河井達治,冨田尭
    • Organizer
      情報処理学会 第205回ソフトウェア工学研究発表会
    • Related Report
      2020 Annual Research Report
  • [Presentation] A Scalable Monte-Carlo Test-Case Generation Tool for Large and Complex Simulink Models2019

    • Author(s)
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • Organizer
      11th Workshop on Modelling in Software Engineering
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Reducing False Positives of Static Analysis for SEI CERT C Coding Standard2019

    • Author(s)
      Thu Trang Nguyen, Pattaravut Maleehuan, Toshiaki Aoki, Takashi Tomita, Iori Yamada
    • Organizer
      Joint International Workshop on Conducting Empirical Studies in Industry and 6th International Workshop on Software Engineering Research and Industrial Practice
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Compaction of Spacecraft Operation Model using Domain Knowledge based Stereotype2019

    • Author(s)
      Kazunori Someya, Naoki Ishihama, Keiichi Wada, Toshiaki Aoki
    • Organizer
      International Symposium on Space Technology and Science
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Conformance Testing of Schedulers for DSL-based Model Checking2019

    • Author(s)
      Nhat-Hoa Tran and Toshiaki Aoki
    • Organizer
      26th International SPIN Symposium on Model Checking of Software
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard2019

    • Author(s)
      Thu-Trang Nguyen, Toshiaki Aoki, Takashi Tomita and Iori Yamada
    • Organizer
      Asia-Pacific Software Engineering Conference
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller2019

    • Author(s)
      Thuy Nguyen, Toshiaki Aoki, Takashi Tomita and Junpei Endo
    • Organizer
      Asia-Pacific Software Engineering Conference
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Model Checking Automotive Systems2019

    • Author(s)
      Toshiaki Aoki
    • Organizer
      Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Event-Bに基づいた鉄道システムの実践的な形式化と検証2019

    • Author(s)
      太田十字光, 青木利晃
    • Organizer
      情報処理学会 第203回ソフトウェア工学研究会
    • Related Report
      2019 Annual Research Report
  • [Presentation] Qualitative and Quantitative Analysis with Scheduling Policies in Model Checking2018

    • Author(s)
      Nhat-Hoa Tran, Yuki Chiba and Toshiaki Aoki
    • Organizer
      The 33rd ACM/SIGAPP Symposium On Applied Computing
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formalization and Verification of AUTOSAR OS Standard's Memory Protection2018

    • Author(s)
      Trinh Le Khanh, Yuki Chiba and Toshiaki Aoki
    • Organizer
      The 12th International Symposium on Theoretical Aspects of Software Engineering
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change2018

    • Author(s)
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • Organizer
      IEEE/ACM the 22nd International Symposium on Distributed Simulation and Real Time Applications
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems2018

    • Author(s)
      Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
    • Organizer
      The 23rd IEEE Pacific Rim International Symposium on Dependable Computing
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 確率統計に基づいた故障木とテストによる機械学習システムの系統的評価手法2018

    • Author(s)
      青木利晃,川上大介,千田伸男,冨田尭
    • Organizer
      ソフトウェアエンジニアリングシンポジウム
    • Related Report
      2018 Annual Research Report
  • [Presentation] 形式手法と安全性2018

    • Author(s)
      青木利晃
    • Organizer
      安全工学会 安全工学研究発表会
    • Related Report
      2018 Annual Research Report
    • Invited
  • [Presentation] 車載システム開発における形式手法実践の現状と課題2018

    • Author(s)
      青木利晃
    • Organizer
      日本ソフトウェア科学会 第16回 ディペンダブルシステムワークショップ
    • Related Report
      2018 Annual Research Report
    • Invited

URL: 

Published: 2018-04-23   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi