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

2023 Fiscal Year Final Research Report

• 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: Yamane Satoshi 金沢大学, 電子情報通信学系, 教授 (70263506)
• Co-Investigator(Kenkyū-buntansha): 櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: 組込みソフトウェア / 割込み処理 / アセンブリプログラム / ソフトウェアモデル検査 / 抽象化精錬 / SMTソルバー / 双模倣関係

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.

Free Research Field

コンピュータソフトウェア

Academic Significance and Societal Importance of the Research Achievements

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