記号実行による組込みアセンブリプログラムのソフトウェアモデル検査

摘要

組込みシステムのソフトウェアモデル検査器を開発した．この検証器は，アセンブリプログラムから，モデルを記号実行を用いて動的に生成し，Z3を用いて，逐次的に到達可能性解析を行うことで，検証を行う．記号実行を用いることで，従来の組込みアセンブリ検証器よりも大きなモデルを検証することが目的としている．また，本研究では，アセンブリプログラムへ記号実行を適用する際の問題点について述べ，今回対象としているハードウェアに適用する方法について述べ，実装を行う．