抄録
本研究ではハイブリッドシステムの到達可能性検証のための有界モデル検査法(bounded model checking)を提案する.提案手法では,非線形ハイブリッドオートマトンを常微分方程式およびガード制約を埋め込んだ論理式として,モデル中の危険領域を示す論理式とともに記述する.上記論理式の充足可能性をSAT求解系と数式処理系(Mathematica)を連携させた探索により示し,モデル中の不具合を発見することができる.
We propose a bounded model checking method for reachability analysis of hybrid systems. In our method, a nonlinear hybrid automaton is encoded into a logic formula which contains ordinary differential equations and guard constraints. The formula is also joined with logic formulas describing unsafe regions in a model. By showing satisfiability of the logic formula with a SAT solver and a computer algebra system (Mathematica), a bug in the model will be detected.
