Tool-support for the analysis of hybrid systems and models

This paper introduces a method and tool-support for the automatic analysis and verification of hybrid and embedded control systems, whose continuous dynamics are often modelled using MATLAB/Simulink. The method is based upon converting system models into the uniform input language of our efficient multi-domain constraint solving library, ABSOLVER, which is then used for subsequent analysis. Basically, ABSOLVER is an extensible SMT-solver which addresses mixed Boolean and (nonlinear) arithmetic constraint problems as they appear in the design of hybrid control systems. It allows the integration and semantic connection of various domain specific solvers via a logical circuit, such that almost arbitrary multi-domain constraint problems can be formulated and solved. Its design has been tailored for extensibility, and thus facilitates the reuse of expert knowledge, in that the most appropriate solver for a given task can be integrated and used. As such the only constraint over the probl...

• Type: Conference
• Year: 2007
• Where: DATE
• Authors: Andreas Bauer 0002, Markus Pister, Michael Tautschnig
• Keywords: Constraint Problems, Control System, DATE 2007, Hardware, Multi-domain Constraint