Direct handling of ordinary differential equations in constraint-solving-based analysis of hybrid systems
Andreas Eggers · Carl von Ossiezky University of Oldenburg · 2014
In this thesis, the behavior of hybrid discrete-continuous systems is analyzed using a Bounded Model Checking (BMC) approach, i.e. by finitely unwinding the systems' transition relations as formulae. Contrary to earlier BMC approaches for hybrid systems, we allow Ordinary Differential Equations (ODEs) directly in the formula, introducing the problem class of Satisfiability (SAT) modulo ODE. The main contribution of the thesis and its underlying publications is the direct handling of SAT modulo ODE formulae by combining the iSAT solver for boolean combinations of non-linear arithmetic constraints with the VNODE-LP library for computing validated numerical enclosures for ODE solutions. This iSAT-ODE solver comprises several algorithmic enhancements, like caching of intermediate results and previous queries, bracketing systems, and the deduction of trajectory directions, all of which are subjected to evaluation on academic case studies and compared with results from the literature.