2020 Fiscal Year Annual Research Report
Software model checking of real-time safety properties for embedded assembly program
| Project/Area Number |
18K11239
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 時間Kripke構造 / SAT/SMT理論 / 抽象化精錬(CEGAR) |
|---|
| Outline of Annual Research Achievements |
本研究では，これまでの研究成果をもとに，組込みアセンブリプログラムのリアルタイム安全性検証を実現するために，以下の分担（代表者 山根がモデル検査の理論実装，分担者 櫻井がプログラム解析）で，申請者らは前年度までに以下の成果を上げた。(①何を ②どのように ③どこまで明らかに)
(1)時間Kripke 構造により，アセンブリプログラムのハードウェアとの相互作用およびタイミング制約の形式的意味の定義（担当：山根）① アセンブリプログラムのハードウェアとの相互作用およびタイミング制約などの形式的意味を時間Kripke 構造で表現した．② アセンブリプログラムから時間Kripke 構造に変換して，さらに検証性質をリアルタイム時相論理で仕様記述した．③現実の組込みアセンブリプログラムの意味及びその検証性質が時間Kripke 構造及びリアルタイム時相論理で表現できることを，理論的及び実験的に明らかにした．
本年度は、上記の前年度の成果をもとに、以下の成果を上げた。
(2)アセンブリプログラムのソフトウェアモデル検査（担当：山根,櫻井,大学院生5 名）① アセンブリプログラムのソフトウェアモデル検査を開発した．② アセンブリプログムのプログラム解析及び述語抽象化からなるSMT 述語抽象化により，時間Kripke 構造の抽象化を行った（担当：櫻井，山根）．③ 抽象時間Kripke 構造のSMT 述語抽象化，SMT 抽象モデル検査，SMT 反例解析，SMT Interpolation（担当：山根）により，組込みアセンブリプログラムのリアルタイム性の抽象化精錬のソフトウェアモデル検査手法を開発した．大学院生5 名と共同で，プロトタイプを実装して，現実の組込みソフトウェアのリアルタイム性の検証が行えることを明らかにした．
|
Research Products
(4 results)
