WEKO3
アイテム
組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発
https://doi.org/10.24517/00057604
https://doi.org/10.24517/00057604051e04b0-c848-400e-8084-6f8a5b1ff830
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YAMANE-S-kaken 2021-6p.pdf (82.6 kB)
|
.png)
|
| アイテムタイプ | 報告書 / Research Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2022-02-10 | |||||
| タイトル | ||||||
| タイトル | 組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発 | |||||
| タイトル | ||||||
| タイトル | Software model checking of real-time safety properties for embedded assembly program | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18ws | |||||
| 資源タイプ | research report | |||||
| ID登録 | ||||||
| ID登録 | 10.24517/00057604 | |||||
| ID登録タイプ | JaLC | |||||
| 著者 |
山根, 智
× 山根, 智 |
|||||
| 提供者所属 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 金沢大学理工研究域電子情報通信学系 | |||||
| 書誌情報 |
令和2(2020)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 en : 2020 Fiscal Year Final Research Report 巻 2018-04-01 - 2021-03-31, p. 6p., 発行日 2021-06-18 |
|||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 本研究では，ハードウェアとの相互作用があり，タイミング制約が厳しい組込みソフトウェアのリアルタイム性の形式的検証を研究目的とする．アセンブリプログラムを対象に，ソフトウェアモデル検査技術を開発し，組込みアセンブリプログラムのリアルタイム安全性検証の開発を研究目的とする．(1)アセンブリプログラムを変換して，組込みソフトウェアの形式的意味モデルである時間Kripke 構造を生成する．(2)定理証明技術を基礎として，SMT述語抽象化，SMTモデル検査及びSMT Interpolationの精錬により，組込みソフトウェアのリアルタイム性のモデル検査技術を開発する． | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | The purpose of this research is to formally verify real-time properties of embedded software that interacts with hardware and has severe timing constraints. The research objectives are to develop software model checking techniques for assembly programs, and to develop real-time safety verification for embedded assembly programs. (1) Transform assembly programs to generate the time Kripke structure, which is a formal semantic model of embedded software. (2) Based on theorem proving techniques, we develop a model checking technique for real-time embedded software by refining SMT predicate abstraction, SMT model checking, and SMT interpolation. | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 研究課題/領域番号:18K11239, 研究期間(年度):2018-04-01 - 2021-03-31 | |||||
| 内容記述 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 出典：「組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発」研究成果報告書 課題番号18K11239 （KAKEN：科学研究費助成事業データベース（国立情報学研究所）） （https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/）を加工して作成 |
|||||
| 著者版フラグ | ||||||
| 出版タイプ | AM | |||||
| 出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/search/?qm=70263506 | |||||
| 関連名称 | https://kaken.nii.ac.jp/search/?qm=70263506 | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18K11239/ | |||||
| 関連名称 | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18K11239/ | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/ | |||||
| 関連名称 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/ | |||||
