@techreport{oai:ipsj.ixsq.nii.ac.jp:00095552,
 author = {公下, 亮佑 and 山根, 智 and 櫻井, 孝平 and Ryousuke, Konoshita and Satoshi, Yamane and Kouhei, Sakurai},
 issue = {2},
 month = {Oct},
 note = {我々は，組込みシステムに対してモデル検査することを目的とする．そこで，本論文では，モデルを自動的に構築する，振舞い抽出器の概要について述べる．また，開発する上で困難となる要因と，解決方法について述べる．この抽出器は，状態爆発を起こす可能性があり，特に割り込みやリアクティブ性が，大きな影響を与えている．割り込みは，マスクビットなどから割り込み発生箇所を特定することができる．そのため，考慮する必要のない割り込みを取り除き，状態爆発を抑制できる．リアクティブ性は，不定値で表現することで状態爆発を軽減する．これは，ある値に対して，ピット単位での抽象的な表現を可能にしたものである．, 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.},
 title = {組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～},
 year = {2013}
}