2018 Fiscal Year Research-status 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 | ソフトウェアモデル検査 / 組込みアセンブリプログラム |
|---|
| Outline of Annual Research Achievements |
H30年度は、以下の手法，理論およびそのツールを開発した．
１．以下の手法と理論を開発した：組込みソフトウェアのハードウェアとの相互作用およびタイミング制約を検証するために，アセンブリプログラムの変数値，スタックやアドレスばかりでなく，命令の実行時間を含めて，時間Kripke 構造（＝組込みソフトウェアの形式的意味モデル）を開発した．さらに，アセンブリプログラムを時間Kripke 構造へ変換する手法を開発した．また，リアルタイム安全性などの検証性質をリアルタイム時相論理で記述した．また，述語抽象化ベースのSMT抽象化手法，SMT抽象モデル検査手法，SMTベースの抽象化精錬手法を開発した．
２．以下のツールを開発した：述語抽象化手法をベースに，SMT 述語抽象化器とSMT 抽象モデル検査器を開発した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
H30年度は、上記の手法，理論およびそのツールを開発した．その成果を以下に発表した．
Yajun Wu, Satoshi Yamane:Model Checking of Embedded Systems Using RTCTL While Generating Timed Kripke Structure. IEEE COMPSAC (1) 2018: 257.
Hiromu Kamide, Kosuke Uemura, Satoshi Yamane:Model Check of Real-time Property of Embedded Assembly Program Using CEGAR. IEEE COMPSAC (1) 2018: 799-800.
|
| Strategy for Future Research Activity |
今後はSMT 反例解器及びSMT Interpolation による抽象化精錬器を開発して，SMTベースの抽象化精錬型のソフトウェアモデル検査器を実現する．
さらに，実用レベルの事例により，計算機実験を行い，提案手法の有効性を実証する．
また，その成果を国際会議及びジャーナルに投稿する．
|
| Causes of Carryover |
研究分担者の消耗品が少額で済んだので、次年度に回します。
|
