2021 Fiscal Year Research-status Report
Software model checking for real-time properties of embedded assembply program with interruptions
| Project/Area Number |
21K11824
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 / 抽象化精錬(CEGAR) |
|---|
| Outline of Annual Research Achievements |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の実現において、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として発表し、優秀論文賞を受賞した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
まず、アセンブリプログラムの静的プログラム解析と動的プログラム解析により，プログラム動作に影響を与えるタイマー割込み処理のみを埋め込んだアセンブリプログラムを自動生成し、その後、時間Kripke構造を自動生成して、到達可能性解析に特化したソフトウェアモデル検査器を実現した。また、その効果を実証した。
次に、SMT (Satisfiability Modulo Theories) と述語抽象精錬手法を用いて、（１）のソフトウェアモデル検査器を拡張しており、2022年3月の時点では、モデル検査器はほぼ完成している。
|
| Strategy for Future Research Activity |
今後は、2023年3月までに、SMT (Satisfiability Modulo Theories) と述語抽象精錬手法を用いて、ソフトウェアモデル検査器を拡張して完成させて、その成果をジャーナルに投稿する。
また、2024年4月より、実際の事例を用いて、検証実験を行い、本研究テーマの有効性を実証する。
|
| Causes of Carryover |
備品の納入が間に合わなかったために、次年度繰り越す。
|
