| 講演名 | 2015-06-18 記号実行による組込みアセンブリプログラムのソフトウェアモデル検査 公下 亮佑(金沢大), 山根 智(金沢大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 組込みシステムのソフトウェアモデル検査器を開発した．この検証器は，アセンブリプログラムから，モデルを記号実行を用いて動的に生成し，逐次的に到達可能性解析を行うことで，検証を行う．記号実行を用いることで，従来の組込みアセンブリ検証器よりも大きなモデルを検証することが目的としている．また，本研究では，アセンブリプログラムへ記号実行を適用する際の問題点について述べ，今回対象としているハードウェアに適用する方法について述べ，実装を行う．最後に，実験を通し，検証できる性質について示す．加えて，従来よりも大きいモデルに対応できることを示す． |
| 抄録(英) | We have developed a software verification system for embedded assembly programs. It dynamically generates a model by the symbolic execution, and verifies the model by a reachability analysis. Our verification system verifies a model bigger than a conventional verification system for embedded systems. We explain a method which applies the symbolic execution to assembly programs. Finally, we show verification properties through some experiments. In addition, we show that our verification system can verify larger models. |
| キーワード(和) | 組込みアセンブリプログラム / ソフトウェアモデル検査 / 記号実行 |
| キーワード(英) | embedded assembly program / software model checking / symbolic execution |
| 資料番号 | CAS2015-15,VLD2015-22,SIP2015-46,MSS2015-15 |
| 発行日 | 2015-06-10 (CAS, VLD, SIP, MSS) |
| 研究会情報 | |
| 研究会 | MSS / CAS / SIP / VLD |
|---|---|
| 開催期間 | 2015/6/17(から2日開催) |
| 開催地（和） | 小樽商科大学 |
| 開催地（英） | Otaru University of Commerce |
| テーマ（和） | システムと信号処理および一般 |
| テーマ（英） | System, signal processing and related topics |
| 委員長氏名（和） | 山根 智(金沢大) / 田中 聡(村田製作所) / 宝珠山 治(NEC) / 松永 裕介(九大) |
| 委員長氏名（英） | Satoshi Yamane(Kanazawa Univ.) / Satoshi Tanaka(Murata) / Osamu Houshuyama(NEC) / Yusuke Matsunaga(Kyushu Univ.) |
| 副委員長氏名（和） | 名嘉村 盛和(琉球大) / 高橋 俊彦(新潟大) / 中静 真(千葉工大) / 奥田 正浩(北九州市大) / 竹中 崇(NEC) |
| 副委員長氏名（英） | Morikazu Nakamura(Univ. of Ryukyus) / Toshihiko Takahashi(Niigata Univ.) / Makoto Nakashizuka(Chiba Inst. of Tech.) / Masahiro Okuda(Univ. of Kitakyushu) / Takashi Takenana(NEC) |
| 幹事氏名（和） | 中田 充(山口大) / 豊嶋 伊知郎(東芝) / 山脇 大造(日立) / 越田 俊介(東北大) / 辻川 剛範(NEC) / 平林 晃(立命館大) / 冨山 宏之(立命館大) / 福田 大輔(富士通研) |
| 幹事氏名（英） | Mitsuru Nakata(Yamaguchi Univ.) / Ichiro Toyoshima(Toshiba) / Taizou Yamawaki(Hitachi) / Shunsuke Koshita(Tohoku Univ.) / Masanori Tsujikawa(NEC) / Akira Hirabayashi(Ritsumeikan Univ.) / Hiroyuki Tomiyama(Ritsumeikan Univ.) / Daisuke Fukuda(Fujitsu Labs.) |
| 幹事補佐氏名（和） | 金城 秀樹(沖縄大) / 橘 俊宏(湘南工科大) / 中村 洋平(日立) / 宮田 高道(千葉工大) / 谷口 一徹(立命館大) |
| 幹事補佐氏名（英） | Hideki Kinjo(Okinawa Univ.) / Toshihiro Tachibana(Shonan Inst. of Tech.) / Yohei Nakamura(Hitachi) / Takamichi Miyata(Chiba Inst. of Tech.) / Ittetsu Taniguchi(Ritsumeikan Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Circuits and Systems / Technical Committee on Signal Processing / Technical Committee on VLSI Design Technologies |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 記号実行による組込みアセンブリプログラムのソフトウェアモデル検査 |
| サブタイトル（和） | |
| タイトル（英） | Software model checking of embedded assembly programs by symbolic execution |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 組込みアセンブリプログラム / embedded assembly program |
| キーワード(2)（和/英） | ソフトウェアモデル検査 / software model checking |
| キーワード(3)（和/英） | 記号実行 / symbolic execution |
| 第 1 著者 氏名（和/英） | 公下 亮佑 / Ryosuke Konoshita |
| 第 1 著者 所属（和/英） | 金沢大学(略称：金沢大) Kanazawa Uuniversity(略称：Kanazawa Univ.) |
| 第 2 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 2 著者 所属（和/英） | 金沢大学(略称：金沢大) Kanazawa Uuniversity(略称：Kanazawa Univ.) |
| 発表年月日 | 2015-06-18 |
| 資料番号 | CAS2015-15,VLD2015-22,SIP2015-46,MSS2015-15 |
| 巻番号（vol） | vol.115 |
| 号番号（no） | CAS-87,VLD-88,SIP-89,MSS-90 |
| ページ範囲 | pp.77-81(CAS), pp.77-81(VLD), pp.77-81(SIP), pp.77-81(MSS), |
| ページ数 | 5 |
| 発行日 | 2015-06-10 (CAS, VLD, SIP, MSS) |