Design Principles for an Extendable Verification Tool for Hybrid Systems

The verification of continuous and hybrid systems is known to be hard, and today tools are limited to relatively small problems. Several novel approaches are currently under investigation that exploit various kinds of set representations (polyhedra, zonotopes), improved algorithms (avoiding the wrapping effect) and strategies (such as abstraction refinement). We outline a tool framework that is able to integrate and combine different elements from these approaches. The framework includes implementations for common functionality (hybrid automata, graphical output, basic set operations, etc.) and interfaces that allow us to plug in different implementations, such as a particular kind of set representation or a particular optimization algorithm. This allows us to experimentally evaluate competing ideas, combine promising elements and explore new approaches with relatively little development effort.