Tool-support for the analysis of hybrid systems and models
Andreas Bauer, Markus Pister, Michael Tautschnig · 2007
Abstract This paper introduces a method and tool-support for theautomatic analysis and verification of hybrid and embedded control systems, whose continuous dynamics are oftenmodelled using MATLAB/Simulink. The method is based upon converting system models into the uniform input lan-guage of our efficient multi-domain constraint solving library, ABSOLVER, which is then used for subsequent anal-ysis. Basically, AB SOLVER is an extensible SMT-solverwhich addresses mixed Boolean and (nonlinear) arithmetic constraint problems as they appear in the design of hy-brid control systems. It allows the integration and semantic connection of various domain specific solvers via a logicalcircuit, such that almost arbitrary multi-domain constraint problems can be formulated and solved. Its design has beentailored for extensibility, and thus facilitates the reuse of expert knowledge, in that the most appropriate solver fora given task can be integrated and used. As such the only constraint over the problem domain is the capability of theemployed solvers. Our approach to systems verification has been validated in an industrial case study using the model ofa car's steering control system. However, additional benchmarks show that other hard instances of problems couldalso be solved by AB SOLVER in respectable time, and thatfor some instances, AB