組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～

• Item type: SIG Technical Reports(1)
• 公開日: 2013-10-17
• タイトル: 組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～
• タイトル / 言語: en
• タイトル: Development of the Behavior Extractor for Assembly Program of Embedded CISC Microcomputer and Adapting to Model Checking - Generating the Model Automatically by Simulation -
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 金沢大学
• 著者所属: 金沢大学
• 著者所属: 金沢大学
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者所属(英): en
• 著者所属(英): Kanazawa University
• 著者名: 公下, 亮佑; 山根, 智; 櫻井, 孝平
• 著者名(英): Ryousuke, Konoshita; Satoshi, Yamane; Kouhei, Sakurai
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 我々は，組込みシステムに対してモデル検査することを目的とする．そこで，本論文では，モデルを自動的に構築する，振舞い抽出器の概要について述べる．また，開発する上で困難となる要因と，解決方法について述べる．この抽出器は，状態爆発を起こす可能性があり，特に割り込みやリアクティブ性が，大きな影響を与えている．割り込みは，マスクビットなどから割り込み発生箇所を特定することができる．そのため，考慮する必要のない割り込みを取り除き，状態爆発を抑制できる．リアクティブ性は，不定値で表現することで状態爆発を軽減する．これは，ある値に対して，ピット単位での抽象的な表現を可能にしたものである．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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 possi bility 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10112981
• 書誌情報: 研究報告ソフトウェア工学（SE）; 巻 2013-SE-182, 号 2, p. 1-6, 発行日 2013-10-17
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会