| 研究課題/領域番号 |
21K11824
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2023年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2022年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2021年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
|
|---|
| キーワード | 組込みソフトウェア / 割込み処理 / アセンブリプログラム / ソフトウェアモデル検査 / 抽象化精錬 / SMTソルバー / 双模倣関係 / イベント割込み / タイマ割込み / 組込みアセンブリプログラム / SMT / SAT/SMT理論 / 抽象化精錬(CEGAR) |
|---|
| 研究開始時の研究の概要 |
「割込み処理を持つ組込みソフトウェアのリアルタイム性検証」という本研究課題の核心をなす学術的「問い」は，プログラム解析により，
(a)プログラム動作に影響する割込み処理のみをアセンブリプログラムに埋め込んで，
(b)タイミング制約やタイマ割込み処理などの組込みソフトウェアの特性を表す形式的意味モデル(時間Kripke 構造)へ変換を行い，
(c)ソフトウェアモデル検査技術(SMT 定理証明による抽象化,抽象モデル検査，反例解析，Interpolation，精錬化)の確立である.
|
| 研究成果の概要 |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象とし、SMTソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行った。具体的にはイベント割込みとタイマ割込みの両方を扱い、それらの割込み処理の削減の理論、実装、評価及び、抽象化精錬によるソフトウェアモデル検査の理論、実装、評価を行った。まず、イベント割込みを対象とし、模倣関係による削減の理論、実装、評価を行い、ソフトウェアモデル検査を実現した。次に、時間割込みを対象とし、時間模倣関係による時間割込み処理の削減の理論、実装、評価を行い、ソフトウェアモデル検査を実現した。
|
| 研究成果の学術的意義や社会的意義 |
（１）学術的意義：ハードウェアとの相互作用及びタイミング制約に関する組込みソフトウェア検証は最重要な未解決問題であり，割込み処理を持つ組込みソフトウェアのリアルタイム性の検証を実現するソフトウェアモデル検査が必須である．「割込み処理を持つ組込みソフトウェアのリアルタイム性検証」という学術的「問い」は，(a)割込み処理をアセンブリプログラムに埋め込んで，(b)タイマ割込み処理などの組込みソフトウェアの特性を表す形式的意味モデルへ変換を行い，(c)ソフトウェアモデル検査技術の確立である．
（２）社会的意義：自動運転などの組込みソフトウェア安全性保証の研究は，社会的に最重要な国際的課題である．
|
