革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証

資料種別: 文書・図像類

著者: 山根, 智ほか

出版者: -

出版年: 2018-04-25

資料形態: デジタル

ページ数・大きさ等: -

NDC: -

すべて見る

資料に関する注記

一般注記：: 金沢大学理工研究域電子情報通信学系研究成果は以下の2つに大別できる．（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．...

書店で探す

全国の図書館の所蔵

国立国会図書館以外の全国の図書館の所蔵状況を表示します。

連携機関・データベースの一覧

所蔵のある図書館から取寄せることが可能かなど、資料の利用方法は、ご自身が利用されるお近くの図書館へご相談ください

その他

金沢大学学術情報リポジトリKURA
デジタル
連携先のサイトで、学術機関リポジトリデータベース（IRDB）（機関リポジトリ）が連携している機関・データベースの所蔵状況を確認できます。
金沢大学学術情報リポジトリKURAのサイトでこの本を確認

書店で探す

書誌情報

この資料の詳細や典拠（同じ主題の資料を指すキーワード、著者名）等を確認できます。

デジタル

資料種別: 文書・図像類
タイトル: 革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証
著者・編者: 山根, 智
Yamane, Satoshi
著者標目: 山根, 智
Yamane, Satoshi
出版年月日等: 2018-04-25
出版年（W3CDTF）: 2018-04-25
並列タイトル等: Verifying safety properties of embedded assembly program using innovative software model checking
タイトル（掲載誌）: 平成29(2017)年度科学研究費補助金基盤研究(C) 研究成果報告書 = 2017 Fiscal Year Final Research Report
巻号年月日等（掲載誌）: 2015-04-01 - 2018-03-31
掲載巻: 2015-04-01 - 2018-03-31
掲載ページ: 4p.-
本文の言語コード: jpn
件名標目: ソフトウェアモデル検査
組込みアセンブリプログラム
抽象化精錬
ＳＭＴ
定理証明
対象利用者: 一般
一般注記: 金沢大学理工研究域電子情報通信学系
研究成果は以下の2つに大別できる．（1）動的プログラム解析の枝刈りと抽象化，実行時間見積もりによる最小なモデル構築器（アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する）を作成した．（2）抽象化精錬(CEGAR)型ＳＭＴモデル検査手法を開発した．このモデル検査手法はＳＭＴによる述語抽象化、ＳＭＴ有界モデル検査、ＳＭＴによる反例解析器、ＳＭＴソルバによるInterpolationを用いた精錬述語の生成からなる．なお、ＳＭＴソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた．
The research outcome can be roughly divided into the following two.(1) We have developed a minimal model constructor (constructing a minimum model with interrupt processing embedded from the assembly program) by pruning and abstraction of dynamic program analysis and execution time estimation.(2) SMT model checking method based on Abstraction and Refinement (CEGAR) was developed. This model checking method consists of predicate abstraction by SMT, SMT bounded model check, counter-example analyzer by SMT, and refinement predicate generation using Interpolation by SMT solver. As the SMT solver, Princess of Uppsala University which supports various interpolations was used.
研究課題/領域番号:15K00093, 研究期間(年度):2015-04-01 - 2018-03-31
出典：研究課題「革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証」課題番号15K00093（KAKEN：科学研究費助成事業データベース（国立情報学研究所））（https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/）を加工して作成
DOI: 10.24517/00053962
一次資料へのリンクURL: https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47638&item_no=1&attribute_id=26&file_no=1
https://kanazawa-u.repo.nii.ac.jp/?action=repository_action_common_download&item_id=47638&item_no=1&attribute_id=26&file_no=1
オンライン閲覧公開範囲: 限定公開
著作権情報: CC BY-NC-ND
関連情報: https://kaken.nii.ac.jp/search/?qm=70263506
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/
https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/
連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
提供元機関・データベース: 金沢大学 : 金沢大学学術情報リポジトリKURA