| 講演名 | 2013-10-24 組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用 : シミュレーションによるモデルの自動生成 公下 亮佑, 山根 智, 櫻井 孝平, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 我々は,組込みシステムに対してモデル検査することを目的とする.そこで,本論文では,モデルを自動的に構築する,振舞い抽出器の概要について述べる. また,開発する上で困難となる要因と,解決方法について述べる.この抽出器は,状態爆発を起こす可能性があり,特に割り込みやリアクティブ性が,大きな影響を与えている.割り込みは,マスクビットなどから割り込み発生箇所を特定することができる.そのため,考慮する必要のない割り込みを取り除き,状態爆発を抑制できる.リアクティブ性は,不定値で表現することで状態爆発を軽減する.これは,ある値に対して,ビット単位での抽象的な表現を可能にしたものである. |
| 抄録(英) | 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 |
| 資料番号 | SS2013-37 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2013/10/17(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 組込み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 |
| 第 1 著者 氏名（和/英） | 公下 亮佑 / Ryousuke KONOSHITA |
| 第 1 著者 所属（和/英） | 金沢大学 Kanazawa University |
| 第 2 著者 氏名（和/英） | 山根 智 / Satoshi YAMANE |
| 第 2 著者 所属（和/英） | 金沢大学 Kanazawa University |
| 第 3 著者 氏名（和/英） | 櫻井 孝平 / Kouhei SAKURAI |
| 第 3 著者 所属（和/英） | 金沢大学 Kanazawa University |
| 発表年月日 | 2013-10-24 |
| 資料番号 | SS2013-37 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | 269 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |