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

Software model checking for real-time properties of embedded assembply program with interruptions

Research Project

Project/Area Number 21K11824
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60050:Software-related
Research InstitutionKanazawa University

Principal Investigator

Yamane Satoshi  金沢大学, 電子情報通信学系, 教授 (70263506)

Co-Investigator(Kenkyū-buntansha) 櫻井 孝平  金沢大学, 電子情報通信学系, 助教 (80597021)
Project Period (FY) 2021-04-01 – 2024-03-31
Project Status Completed (Fiscal Year 2023)
Budget Amount *help
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Keywords組込みソフトウェア / 割込み処理 / アセンブリプログラム / ソフトウェアモデル検査 / 抽象化精錬 / SMTソルバー / 双模倣関係 / イベント割込み / タイマ割込み / 組込みアセンブリプログラム / SMT / SAT/SMT理論 / 抽象化精錬(CEGAR)
Outline of Research at the Start

「割込み処理を持つ組込みソフトウェアのリアルタイム性検証」という本研究課題の核心をなす学術的「問い」は,プログラム解析により,
(a)プログラム動作に影響する割込み処理のみをアセンブリプログラムに埋め込んで,
(b)タイミング制約やタイマ割込み処理などの組込みソフトウェアの特性を表す形式的意味モデル(時間Kripke 構造)へ変換を行い,
(c)ソフトウェアモデル検査技術(SMT 定理証明による抽象化,抽象モデル検査,反例解析,Interpolation,精錬化)の確立である.

Outline of Final Research Achievements

Theoretical and implementation studies of software model checking of real-time performance of embedded assembly programs with interrupts were conducted using the SMT solver, and the realization and evaluation of software model checking by abstraction refinement were studied. Specifically, both event interrupts and time interrupts were treated, and the theory, implementation, and evaluation of reduction of their interrupt processing, as well as the theory, implementation, and evaluation of software model checking by abstraction refinement were conducted.
First, we addressed event interrupts, and conducted the theory, implementation, and evaluation of reduction by imitation relations to realize software model checking.
Second, for time interrupt, the theory, implementation, and evaluation of reduction of time interrupt processing by the time imitation relation were conducted, and software model checking was realized.

Academic Significance and Societal Importance of the Research Achievements

(1)学術的意義:ハードウェアとの相互作用及びタイミング制約に関する組込みソフトウェア検証は最重要な未解決問題であり,割込み処理を持つ組込みソフトウェアのリアルタイム性の検証を実現するソフトウェアモデル検査が必須である.「割込み処理を持つ組込みソフトウェアのリアルタイム性検証」という学術的「問い」は,(a)割込み処理をアセンブリプログラムに埋め込んで,(b)タイマ割込み処理などの組込みソフトウェアの特性を表す形式的意味モデルへ変換を行い,(c)ソフトウェアモデル検査技術の確立である.
(2)社会的意義:自動運転などの組込みソフトウェア安全性保証の研究は,社会的に最重要な国際的課題である.

Report

(4 results)
  • 2023 Annual Research Report   Final Research Report ( PDF )
  • 2022 Research-status Report
  • 2021 Research-status Report
  • Research Products

    (3 results)

All 2024 2023 2021

All Journal Article (3 results) (of which Peer Reviewed: 2 results,  Open Access: 1 results)

  • [Journal Article] An Efficient Reduction of Timer Interrupts for Model Checking of Embedded Assembly Programs2024

    • Author(s)
      Satoshi Yamane , Taro Kriyama , Yajun Wu
    • Journal Title

      Electronics

      Volume: 13 Issue: 2 Pages: 1-12

    • DOI

      10.3390/electronics13020463

    • Related Report
      2023 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] 有界モデル検査を用いたリアルタイムOSカーネルのタスク管理モジュールの形式的検証2023

    • Author(s)
      小柴真之介、山根智
    • Journal Title

      情報処理学会ソフトウェア工学研究会

      Volume: SE-213 Pages: 1-8

    • Related Report
      2022 Research-status Report
  • [Journal Article] Reduction of Timer Interrupts for Embedded Assembly Programs Based on Reduction of Interrupt Handler Executions2021

    • Author(s)
      Taro Kiriyama, Yajun Wu, Satoshi Yamane
    • Journal Title

      2021 IEEE 10th Global Conference on Consumer Electronics (GCCE)

      Volume: 10 Pages: 464-466

    • DOI

      10.1109/gcce53005.2021.9622013

    • Related Report
      2021 Research-status Report
    • Peer Reviewed

URL: 

Published: 2021-04-28   Modified: 2025-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi