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

摘要

我々は，組込みシステムに対してモデル検査することを目的とする．そこで，本論文では，モデルを自動的に構築する，振舞い抽出器の概要について述べる．また，開発する上で困難となる要因と，解決方法について述べる．この抽出器は，状態爆発を起こす可能性があり，特に割り込みやリアクティブ性が，大きな影響を与えている．割り込みは，マスクビットなどから割り込み発生箇所を特定することができる．そのため，考慮する必要のない割り込みを取り除き，状態爆発を抑制できる．リアクティブ性は，不定値で表現することで状態爆発を軽減する．これは，ある値に対して，ビット単位での抽象的な表現を可能にしたものである．