WEKO3
インデックスリンク
アイテム
{"_buckets": {"deposit": "e20abf32-867f-4444-a544-242c230f3795"}, "_deposit": {"created_by": 18, "id": "47638", "owners": [18], "pid": {"revision_id": 0, "type": "depid", "value": "47638"}, "status": "published"}, "_oai": {"id": "oai:kanazawa-u.repo.nii.ac.jp:00047638", "sets": ["2816"]}, "author_link": ["397", "84982"], "item_9_biblio_info_8": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2018-04-25", "bibliographicIssueDateType": "Issued"}, "bibliographicPageStart": "4p.", "bibliographicVolumeNumber": "2015-04-01 - 2018-03-31", "bibliographic_titles": [{"bibliographic_title": "平成29(2017)年度 科学研究費補助金 基盤研究(C) 研究成果報告書"}, {"bibliographic_title": "2017 Fiscal Year Final Research Report", "bibliographic_titleLang": "en"}]}]}, "item_9_creator_33": {"attribute_name": "著者別表示", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Yamane, Satoshi"}], "nameIdentifiers": [{"nameIdentifier": "84982", "nameIdentifierScheme": "WEKO"}, {"nameIdentifier": "70263506", "nameIdentifierScheme": "e-Rad", "nameIdentifierURI": "https://kaken.nii.ac.jp/ja/search/?qm=70263506"}]}]}, "item_9_description_21": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": " 研究成果は以下の2つに大別できる.\n(1)動的プログラム解析の枝刈りと抽象化,実行時間見積もりによる最小なモデル構築器(アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する)を作成した.\n(2)抽象化精錬(CEGAR)型SMTモデル検査手法を開発した.このモデル検査手法はSMTによる述語抽象化、SMT有界モデル検査、SMTによる反例解析器、SMTソルバによるInterpolationを用いた精錬述語の生成からなる.なお、SMTソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた.", "subitem_description_type": "Abstract"}, {"subitem_description": "The research outcome can be roughly divided into the following two.\n(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.\n(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.", "subitem_description_type": "Abstract"}]}, "item_9_description_22": {"attribute_name": "内容記述", "attribute_value_mlt": [{"subitem_description": "研究課題/領域番号:15K00093, 研究期間(年度):2015-04-01 - 2018-03-31", "subitem_description_type": "Other"}, {"subitem_description": "出典:研究課題「革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証」課題番号15K00093\n(KAKEN:科学研究費助成事業データベース(国立情報学研究所)) \n(https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/)を加工して作成", "subitem_description_type": "Other"}]}, "item_9_description_5": {"attribute_name": "提供者所属", "attribute_value_mlt": [{"subitem_description": "金沢大学 理工研究域電子情報通信学系 ", "subitem_description_type": "Other"}]}, "item_9_identifier_registration": {"attribute_name": "ID登録", "attribute_value_mlt": [{"subitem_identifier_reg_text": "10.24517/00053962", "subitem_identifier_reg_type": "JaLC"}]}, "item_9_relation_28": {"attribute_name": "関連URI", "attribute_value_mlt": [{"subitem_relation_name": [{"subitem_relation_name_text": "https://kaken.nii.ac.jp/search/?qm=70263506"}], "subitem_relation_type_id": {"subitem_relation_type_id_text": "https://kaken.nii.ac.jp/search/?qm=70263506", "subitem_relation_type_select": "URI"}}, {"subitem_relation_name": [{"subitem_relation_name_text": "https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/"}], "subitem_relation_type_id": {"subitem_relation_type_id_text": "https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/", "subitem_relation_type_select": "URI"}}, {"subitem_relation_name": [{"subitem_relation_name_text": "https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/"}], "subitem_relation_type_id": {"subitem_relation_type_id_text": "https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/", "subitem_relation_type_select": "URI"}}]}, "item_9_version_type_25": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_ab4af688f83e57aa", "subitem_version_type": "AM"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "山根, 智"}], "nameIdentifiers": [{"nameIdentifier": "397", "nameIdentifierScheme": "WEKO"}, {"nameIdentifier": "70263506", "nameIdentifierScheme": "金沢大学研究者情報", "nameIdentifierURI": "http://ridb.kanazawa-u.ac.jp/public/detail.php?kaken=70263506"}, {"nameIdentifier": "70263506", "nameIdentifierScheme": "研究者番号", "nameIdentifierURI": "https://nrid.nii.ac.jp/nrid/1000070263506"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2019-05-13"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "TE-PR-YAMANE-S-kaken 2018-4p.pdf", "filesize": [{"value": "83.2 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_11", "mimetype": "application/pdf", "size": 83200.0, "url": {"label": "TE-PR-YAMANE-S-kaken 2018-4p.pdf", "url": "https://kanazawa-u.repo.nii.ac.jp/record/47638/files/TE-PR-YAMANE-S-kaken 2018-4p.pdf"}, "version_id": "4c4f52d7-bf96-4fa6-88d7-8dec17c191db"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "ソフトウェアモデル検査", "subitem_subject_scheme": "Other"}, {"subitem_subject": "組込みアセンブリプログラム", "subitem_subject_scheme": "Other"}, {"subitem_subject": "抽象化精錬", "subitem_subject_scheme": "Other"}, {"subitem_subject": "SMT", "subitem_subject_scheme": "Other"}, {"subitem_subject": "定理証明", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "research report", "resourceuri": "http://purl.org/coar/resource_type/c_18ws"}]}, "item_title": "革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証"}, {"subitem_title": "Verifying safety properties of embedded assembly program using innovative software model checking", "subitem_title_language": "en"}]}, "item_type_id": "9", "owner": "18", "path": ["2816"], "permalink_uri": "https://doi.org/10.24517/00053962", "pubdate": {"attribute_name": "公開日", "attribute_value": "2019-05-13"}, "publish_date": "2019-05-13", "publish_status": "0", "recid": "47638", "relation": {}, "relation_version_is_last": true, "title": ["革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証"], "weko_shared_id": -1}
革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証
https://doi.org/10.24517/00053962
https://doi.org/10.24517/000539624cc02a9c-8041-48fb-977b-0d5428f255e7
名前 / ファイル | ライセンス | アクション |
---|---|---|
TE-PR-YAMANE-S-kaken 2018-4p.pdf (83.2 kB)
|
Item type | 報告書 / Research Paper(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2019-05-13 | |||||
タイトル | ||||||
タイトル | 革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証 | |||||
タイトル | ||||||
言語 | en | |||||
タイトル | Verifying safety properties of embedded assembly program using innovative software model checking | |||||
言語 | ||||||
言語 | jpn | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_18ws | |||||
資源タイプ | research report | |||||
ID登録 | ||||||
ID登録 | 10.24517/00053962 | |||||
ID登録タイプ | JaLC | |||||
著者別表示 |
Yamane, Satoshi
× Yamane, Satoshi |
|||||
提供者所属 | ||||||
内容記述タイプ | Other | |||||
内容記述 | 金沢大学 理工研究域電子情報通信学系 | |||||
書誌情報 |
平成29(2017)年度 科学研究費補助金 基盤研究(C) 研究成果報告書 en : 2017 Fiscal Year Final Research Report 巻 2015-04-01 - 2018-03-31, p. 4p., 発行日 2018-04-25 |
|||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | 研究成果は以下の2つに大別できる. (1)動的プログラム解析の枝刈りと抽象化,実行時間見積もりによる最小なモデル構築器(アセンブリプログラムから割込み処理が埋め込まれた最小モデルを構築する)を作成した. (2)抽象化精錬(CEGAR)型SMTモデル検査手法を開発した.このモデル検査手法はSMTによる述語抽象化、SMT有界モデル検査、SMTによる反例解析器、SMTソルバによるInterpolationを用いた精錬述語の生成からなる.なお、SMTソルバとして、種々のInterpolationをサポートしているUppsala大学のPrincessを用いた. |
|||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | 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. |
|||||
内容記述 | ||||||
内容記述タイプ | Other | |||||
内容記述 | 研究課題/領域番号:15K00093, 研究期間(年度):2015-04-01 - 2018-03-31 | |||||
内容記述 | ||||||
内容記述タイプ | Other | |||||
内容記述 | 出典:研究課題「革新的ソフトウェアモデル検査による組込みアセンブリプログラムの安全性検証」課題番号15K00093 (KAKEN:科学研究費助成事業データベース(国立情報学研究所)) (https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/)を加工して作成 |
|||||
著者版フラグ | ||||||
出版タイプ | 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-15K00093/ | |||||
関連名称 | https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/ | |||||
関連URI | ||||||
識別子タイプ | URI | |||||
関連識別子 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/ | |||||
関連名称 | https://kaken.nii.ac.jp/report/KAKENHI-PROJECT-15K00093/15K00093seika/ |