組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発

Material type: 文書・図像類

Author: 山根, 智ほか

Publisher: -

Publication date: 2021-06-18

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 金沢大学理工研究域電子情報通信学系本研究では，ハードウェアとの相互作用があり，タイミング制約が厳しい組込みソフトウェアのリアルタイム性の形式的検証を研究目的とする．アセンブリプログラムを対象に，ソフトウェアモデル検査技術を開発し，組込みアセンブリプログラムのリアルタイム安全性検証の開発を研究目的とす...

Related materials as well as pre- and post-revision versions

https://kaken.nii.ac.jp/search/?qm=70263506

https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18K11239/

https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

Kanazawa University Repository for Academic Resources
Digital
You can check the holdings of institutions and databases with which Institutional Repositories DataBase(IRDB)(Institutional Repository) is linked at the site of Institutional Repositories DataBase(IRDB)(Institutional Repository).
Kanazawa University Repository for Academic Resources

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発
Author/Editor: 山根, 智
Yamane, Satoshi
Author Heading: 山根, 智
Yamane, Satoshi
Publication Date: 2021-06-18
Publication Date (W3CDTF): 2021-06-18
Alternative Title: Software model checking of real-time safety properties for embedded assembly program
Periodical title: 令和2(2020)年度科学研究費補助金基盤研究(C) 研究成果報告書 = 2020 Fiscal Year Final Research Report
No. or year of volume/issue: 2018-04-01 - 2021-03-31
Volume: 2018-04-01 - 2021-03-31
Pages: 6p.-
Text Language Code: jpn
Subject Heading: ソフトウェアモデル検査
組込みアセンブリプログラム
抽象化精錬
SMT
Interpolation
Target Audience: 一般
Note (General): 金沢大学理工研究域電子情報通信学系
本研究では，ハードウェアとの相互作用があり，タイミング制約が厳しい組込みソフトウェアのリアルタイム性の形式的検証を研究目的とする．アセンブリプログラムを対象に，ソフトウェアモデル検査技術を開発し，組込みアセンブリプログラムのリアルタイム安全性検証の開発を研究目的とする．(1)アセンブリプログラムを変換して，組込みソフトウェアの形式的意味モデルである時間Kripke 構造を生成する．(2)定理証明技術を基礎として，SMT述語抽象化，SMTモデル検査及びSMT Interpolationの精錬により，組込みソフトウェアのリアルタイム性のモデル検査技術を開発する．
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.
研究課題/領域番号:18K11239, 研究期間(年度):2018-04-01 - 2021-03-31
出典：「組込みアセンブリプログラムのリアルタイム安全性のソフトウェアモデル検査手法の開発」研究成果報告書　課題番号18K11239（KAKEN：科学研究費助成事業データベース（国立情報学研究所））（https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/）を加工して作成
DOI: 10.24517/00057604
Access Restrictions: 限定公開
Related Material: https://kaken.nii.ac.jp/search/?qm=70263506
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18K11239/
https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-18K11239/18K11239seika/
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 金沢大学 : 金沢大学学術情報リポジトリKURA