| 研究課題/領域番号 |
21K11824
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021) [辞退]
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 |
|---|
| 研究実績の概要 |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、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）のスケジューリングの優先度逆転現象の形式的検証を行い、有効性を実証した。現在、ジャーナルへの投稿を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の実現と評価の研究において、ソフトウェアモデル検査を実現して、実験的評価を行い、論文誌へ投稿予定である。また、ソフトウェアモデル検査のフロントエンド処理として、タイマ割込みを削減する手法を実装して、実験的に評価を行い、現在、論文誌への投稿を行った。
また、リアルタイムOSのスケジューリングの形式的検証を行い、有効性を実証して、論文誌へ投稿を行った。
|
| 今後の研究の推進方策 |
今後は、投稿中及び投稿予定の論文誌の1回目の査読が完了したら、追加実験などの論文の改善を行い、採録へ向けての作業を行う。また、開発したソフトウェアモデル検査の実用的な他の事例の検証を行う予定である。
|
| 次年度使用額が生じた理由 |
備品の納入が遅れたため。
|
