DOI:
Abstract:
Though the hybrid system model checker HYTECH has successfully verified some systems, it restricts the dynamics to linear hybrid automata. We have designed an algorithm capable of verifying systems with more general dynamics. This algorithm uses interval numerical methods to conservatively overapproximate the reachable states of a hybrid automaton. We have implemented our new algorithm in HYTECH+. Using three examples, we demonstrate that this algorithm enables both a more accurate and a more direct analysis of hybrid systems.