| 研究課題/領域番号 |
18K11239
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報通信学系, 教授 (70263506)
|
|---|
| 研究分担者 |
櫻井 孝平 金沢大学, 電子情報通信学系, 助教 (80597021)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2018年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
|
|---|
| キーワード | ソフトウェアモデル検査 / 組込みアセンブリプログラム / 抽象化精錬 / SMT / Interpolation / 時間Kripke構造 / SAT/SMT理論 / 抽象化精錬(CEGAR) / リアルタイム安全性 |
|---|
| 研究成果の概要 |
本研究では，ハードウェアとの相互作用があり，タイミング制約が厳しい組込みソフトウェアのリアルタイム性の形式的検証を研究目的とする．アセンブリプログラムを対象に，ソフトウェアモデル検査技術を開発し，組込みアセンブリプログラムのリアルタイム安全性検証の開発を研究目的とする．(1)アセンブリプログラムを変換して，組込みソフトウェアの形式的意味モデルである時間Kripke 構造を生成する．(2)定理証明技術を基礎として，SMT述語抽象化，SMTモデル検査及びSMT Interpolationの精錬により，組込みソフトウェアのリアルタイム性のモデル検査技術を開発する．
|
| 研究成果の学術的意義や社会的意義 |
現在のトヨタ車などのプログラム不具合の解消及び，今後の大規模ソフトウェアからなる
自動運転の安全性確保などの問題もあり，組込みソフトウェア安全性保証の研究は，社会的
かつ科学技術上の最重要な国際的課題である．従来の研究は仕様やＣプログラムの検証であり，組込みソフトウェアのハードウェアとの相互作用の検証やタイミング制約の検証が不十分である．本研究では，ハードウェアとの相互作用及びタイミング制約を検証するために，アセンブリプログラムを，形式的意味モデルである時間Kripke構造（アセンブリ命令の実行時間付き状態遷移システム）に変換して,リアルタイム性のソフトウェアモデル検査手法を開発することである
|
