The Community for Technology Leaders
Design, Automation & Test in Europe Conference & Exhibition (2007)
Nice
Apr. 16, 2007 to Apr. 20, 2007
ISBN: 978-3-9810801-2-4
pp: 172
M. Pister , Inst. fur Informatik, Technische Univ. Munchen
M. Tautschnig , Inst. fur Informatik, Technische Univ. Munchen
A. Bauer , Inst. fur Informatik, Technische Univ. Munchen
ABSTRACT
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 problem domain is the capability of the employed solvers. Our approach to systems verification has been validated in an industrial case study using the model of a car's steering control system. However, additional benchmarks show that other hard instances of problems could also be solved by ABSOLVER in respectable time, and that for some instances, ABsOLVER's approach was the only means of solving a problem at all
INDEX TERMS
car's steering control system, tool-support, hybrid control systems, embedded control systems, MATLAB/Simulink, multidomain constraint solving library, ABSOLVER, Boolean constraint problems, arithmetic constraint problems, domain specific solvers, logical circuit
CITATION
M. Pister, M. Tautschnig, A. Bauer, "Tool-support for the analysis of hybrid systems and models", Design, Automation & Test in Europe Conference & Exhibition, vol. 00, no. , pp. 172, 2007, doi:10.1109/DATE.2007.364411
91 ms
(Ver 3.3 (11022016))