2023 Fiscal Year Annual Research 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) [Withdrawn]
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | イベント割込み / タイマ割込み / 組込みアセンブリプログラム / ソフトウェアモデル検査 / 抽象化精錬 / SMT / 双模倣関係 |
|---|
| Outline of Annual Research Achievements |
本研究では、イベント割込みとタイマ割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、SMT（Satisfiable Modulo Theories）ソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行っている。
具体的には、本研究では、組込みアセンブリプログラムを対象として、イベント割込みとタイマ割込みの両方を扱い、双模倣関係を用いた割込み処理の削減の理論的解析と、SMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査の理論、実装、評価を行っている。
2021年度、2022年の２年間では、イベント割込みを対象として、模倣関係による削減の理論、実装、評価を行い、そのSMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査を実現している。
最終年度の2023年度では、タイマ割込みを対象として、時間模倣関係による時間割込み処理の削減手法の理論、実装、評価を行った。その成果をIEEEの国際会議に採録されて発表した。さらに、最終版を国際ジャーナルに投稿して、国際ジャーナルに採録され、出版された。
現在は、本研究の最終成果として、イベント割込みとタイマ割込みの両方を持つ組込みアセンブリプログラムの割込み削減と、その抽象化精錬によるソフトウェアモデル検査による実問題への適用に取り組んでおり、ジャーナル投稿を予定している。
|
