2022 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) [Withdrawn]
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 |
|---|
| Outline of Annual Research Achievements |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、SMT（Satisfiable Modulo Theories）ソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行っている。
2022年度はおおむね目標通り、以下の（１）組込みアセンブリプログラムのSMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査器の実現、（２）時間模倣関係理論による割込み処理の削減、（３）リアルタイムオペレーティングシステムのスケジューリングの形式的検証、を行った：
（１）組込みアセンブリプログラムを対象とした、昨年度までに実現している、SMT定理証明器を用いた、抽象化精錬によるソフトウェアモデル検査器の実装とロボットアセンブリプログラムによる検証実験を行った。現在、理論と実証実験を含めた論文を作成して、ジャーナルへの投稿を準備している。
（２）ソフトウェアモデル検査のフロントエンド処理として、時間模倣関係理論をもとに実現した、タイマ割込みを削減する手法を実装して、ソフトウェアモデル検査の効率化を実現した。ロボットアセンブリプログラムを対象に実験的に評価を行った。現在、ジャーナルへの投稿を行った。
（３）カーネギーメロン大学とオックスフォート大学の共同開発のSMT/SATによるソフトウェアモデル検査器CBMC（Bounded Model Checker for C and C++ programs）を用いて、名古屋大学で開発・運用しているリアルタイムオペレーティングシステムTOPPERS（Toyohashi Open Platform for Embedded Real-time Systems）のスケジューリングの優先度逆転現象の形式的検証を行い、有効性を実証した。現在、ジャーナルへの投稿を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の実現と評価の研究において、ソフトウェアモデル検査を実現して、実験的評価を行い、論文誌へ投稿予定である。また、ソフトウェアモデル検査のフロントエンド処理として、タイマ割込みを削減する手法を実装して、実験的に評価を行い、現在、論文誌への投稿を行った。
また、リアルタイムOSのスケジューリングの形式的検証を行い、有効性を実証して、論文誌へ投稿を行った。
|
| Strategy for Future Research Activity |
今後は、投稿中及び投稿予定の論文誌の1回目の査読が完了したら、追加実験などの論文の改善を行い、採録へ向けての作業を行う。また、開発したソフトウェアモデル検査の実用的な他の事例の検証を行う予定である。
|
| Causes of Carryover |
備品の納入が遅れたため。
|
