• 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

山根 智  金沢大学, 電子情報通信学系, 教授 (70263506)

Co-Investigator(Kenkyū-buntansha) 櫻井 孝平  金沢大学, 電子情報通信学系, 助教 (80597021)
Project Period (FY) 2021-04-01 – 2024-03-31
Project Status Granted (Fiscal Year 2021)
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ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 / 抽象化精錬(CEGAR)
Outline of Research at the Start

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

URL: 

Published: 2021-04-28   Modified: 2021-08-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi