SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察

摘要

近年，記号モデル検査［1］の有効な手法として命題論理式の充足可能性問題（satisfiability，SAT）を利用する有界モデル検査が注目を集めている．データを含む分散システムの有界モデル検査手法において，SATソルバーではなくSMTソルバー（SAT modulo theories）を用いるとより効率的であることが知られている．また，我々はSOA に基づくシステムを設計·検証するためのUMLサブセットとして，cbUMLを提案した．よって本論文では，cbUML における状態機械のSMTソルバーを用いる有界モデル検査手法を考察する．