| 研究課題/領域番号 |
21K11824
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 / 抽象化精錬(CEGAR) |
|---|
| 研究実績の概要 |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の実現において、2021 年度内に，目標通り、以下を実現した。
（１）まず、アセンブリプログラムの静的プログラム解析と動的プログラム解析により，プログラム動作に影響を与えるタイマー割込み処理のみを埋め込んだアセンブリプログラムを自動生成し、その後、時間Kripke構造を自動生成して、到達可能性解析に特化したソフトウェアモデル検査器を実現して、検証の効率化を実証した。
（２）次に、SMT (Satisfiability Modulo Theories) と述語抽象精錬手法を用いて、（１）のソフトウェアモデル検査器を拡張しており、2022年3月の時点では、モデル検査器はほぼ完成しており、デバッグ中である。
なお、（1）の成果を、国際会議2021 IEEE 10th Global Conference on Consumer Electronics (GCCE)で、論文題名Reduction of Timer Interrupts for Embedded Assembly Programs Based on Reduction of Interrupt Handler Executionsとして発表し、優秀論文賞を受賞した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
まず、アセンブリプログラムの静的プログラム解析と動的プログラム解析により，プログラム動作に影響を与えるタイマー割込み処理のみを埋め込んだアセンブリプログラムを自動生成し、その後、時間Kripke構造を自動生成して、到達可能性解析に特化したソフトウェアモデル検査器を実現した。また、その効果を実証した。
次に、SMT (Satisfiability Modulo Theories) と述語抽象精錬手法を用いて、（１）のソフトウェアモデル検査器を拡張しており、2022年3月の時点では、モデル検査器はほぼ完成している。
|
| 今後の研究の推進方策 |
今後は、2023年3月までに、SMT (Satisfiability Modulo Theories) と述語抽象精錬手法を用いて、ソフトウェアモデル検査器を拡張して完成させて、その成果をジャーナルに投稿する。
また、2024年4月より、実際の事例を用いて、検証実験を行い、本研究テーマの有効性を実証する。
|
| 次年度使用額が生じた理由 |
備品の納入が間に合わなかったために、次年度繰り越す。
|
