Software model checking for real-time properties of embedded assembply program with interruptions
Project/Area Number |
21K11824
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Review Section |
Basic Section 60050:Software-related
|
Research Institution | Kanazawa University |
Principal Investigator |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
Project Period (FY) |
2021-04-01 – 2024-03-31
|
Project Status |
Granted (Fiscal Year 2022)
|
Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
|
Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 割込み処理 / SAT/SMT理論 / 抽象化精錬(CEGAR) |
Outline of Research at the Start |
「割込み処理を持つ組込みソフトウェアのリアルタイム性検証」という本研究課題の核心をなす学術的「問い」は,プログラム解析により, (a)プログラム動作に影響する割込み処理のみをアセンブリプログラムに埋め込んで, (b)タイミング制約やタイマ割込み処理などの組込みソフトウェアの特性を表す形式的意味モデル(時間Kripke 構造)へ変換を行い, (c)ソフトウェアモデル検査技術(SMT 定理証明による抽象化,抽象モデル検査,反例解析,Interpolation,精錬化)の確立である.
|
Outline of Annual Research Achievements |
割込みを持つ組込みアセンブリプログラムのリアルタイム性のソフトウェアモデル検査の理論と実装の研究を対象として、SMT(Satisfiable Modulo Theories)ソルバーを用いて、抽象化精錬によるソフトウェアモデル検査の実現と評価の研究を行っている。 2022年度はおおむね目標通り、以下の(1)組込みアセンブリプログラムのSMTソルバーを用いた抽象化精錬によるソフトウェアモデル検査器の実現、(2)時間模倣関係理論による割込み処理の削減、(3)リアルタイムオペレーティングシステムのスケジューリングの形式的検証、を行った: (1)組込みアセンブリプログラムを対象とした、昨年度までに実現している、SMT定理証明器を用いた、抽象化精錬によるソフトウェアモデル検査器の実装とロボットアセンブリプログラムによる検証実験を行った。現在、理論と実証実験を含めた論文を作成して、ジャーナルへの投稿を準備している。 (2)ソフトウェアモデル検査のフロントエンド処理として、時間模倣関係理論をもとに実現した、タイマ割込みを削減する手法を実装して、ソフトウェアモデル検査の効率化を実現した。ロボットアセンブリプログラムを対象に実験的に評価を行った。現在、ジャーナルへの投稿を行った。 (3)カーネギーメロン大学とオックスフォート大学の共同開発の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回目の査読が完了したら、追加実験などの論文の改善を行い、採録へ向けての作業を行う。また、開発したソフトウェアモデル検査の実用的な他の事例の検証を行う予定である。
|
Report
(2 results)
Research Products
(2 results)