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