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 Type	Multi-year Fund
Section	一般
Review Section	Basic Section 60050:Software-related
Research Institution	Kanazawa 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，精錬化)の確立である.