| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2013-10-24 10:50 組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用 ～ シミュレーションによるモデルの自動生成 ～ ○公下亮佑・山根 智・櫻井孝平（金沢大）  SS2013-37 |
|
| 抄録 | （和） | 我々は，組込みシステムに対してモデル検査することを目的とする．そこで，本論文では，モデルを自動的に構築する，振舞い抽出器の概要について述べる． また，開発する上で困難となる要因と，解決方法について述べる．この抽出器は，状態爆発を起こす可能性があり，特に割り込みやリアクティブ性が，大きな影響を与えている．割り込みは，マスクビットなどから割り込み発生箇所を特定することができる．そのため，考慮する必要のない割り込みを取り除き，状態爆発を抑制できる．リアクティブ性は，不定値で表現することで状態爆発を軽減する．これは，ある値に対して，ビット単位での抽象的な表現を可能にしたものである． |
| （英） | We aim at Model Checking for Embedded Systems. We describe the outline of Behavior Extractor that automatically constructs a model. Also we describe factors that make it difficult to develop. Extractor have possibility of the state explosion. In particular, interruption and reactive nature affect it. Interruption can be specified by masking bits. Therefore, it is possible to remove unnecessary interruption and to avoid the state explosion. Reactive nature is represented by Undefined Value, and it can decrease possibility of the state explosion. It is enabled by abstract representation of a bit-by-bit for certain values. | |
| キーワード | （和） | モデル検査 / 組込みシステム / 動的プログラム解析 / アセンブリプログラム / / / / |
| （英） | Model Checking / Embedded System / Dynamic Program Analysis / Assembly Program / / / / | |
| 文献情報 | 信学技報, vol. 113, no. 269, SS2013-37, pp. 7-12, 2013年10月. | |
| 資料番号 | SS2013-37 | |
| 発行日 | 2013-10-17 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2013-37 |
|
| 研究会情報 | |
| 研究会 | SS IPSJ-SE |
| 開催期間 | 2013-10-24 - 2013-10-25 |
| 開催地（和） | ITビジネスプラザ武蔵（金沢市内） |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2013-10-SS-SE |
| 本文の言語 | 日本語 |
| タイトル（和） | 組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用 |
| サブタイトル（和） | シミュレーションによるモデルの自動生成 |
| タイトル（英） | Development of the Behavior Extractor for Assembly Program of Embedded CISC Microcomputer and Adapting to Model Checking |
| サブタイトル（英） | Generating the Model Automatically by Simulation |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 組込みシステム / Embedded System |
| キーワード(3)（和/英） | 動的プログラム解析 / Dynamic Program Analysis |
| キーワード(4)（和/英） | アセンブリプログラム / Assembly Program |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 公下 亮佑 / Ryosuke Konoshita / コノシタ リョウスケ |
| 第1著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 山根 智 / Satoshi Yamane / ヤマネ サトシ |
| 第2著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 櫻井 孝平 / Kohei Sakurai / サクライ コウヘイ |
| 第3著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2013-10-24 10:50:00 |
| 発表時間 | 20分 |
| 申込先研究会 | SS |
| 資料番号 | SS2013-37 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | no.269 |
| ページ範囲 | pp.7-12 |
| ページ数 | 6 |
| 発行日 | 2013-10-17 (SS) |
[研究会発表申込システムのトップページに戻る]