Paper Info
Title
Tool-support for the analysis of hybrid systems and models
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.
Year
DOI
Venue
2007
10.1109/DATE.2007.364411
DATE
Keywords
Field
DocType
systems verification,hybrid control system,arithmetic constraint problem,hybrid system,embedded control system,efficient multi-domain constraint,arbitrary multi-domain constraint problem,automatic analysis,specific solvers,problem domain,steering control system,automatic control,embedded systems,computability,system modeling,circuits,arithmetic,cntfet,control systems,boolean functions,carbon nanotube,fault detection,formal verification,mathematical model,control system,nanotechnology
Boolean function,Problem domain,Computer science,Computability,Theoretical computer science,Boolean algebra,Control system,Solver,Hybrid system,Formal verification
Conference
ISSN
ISBN
Citations 
1530-1591
978-3-9810801-2-4
25
PageRank 
References 
Authors
1.23
10
3
Name
Order
Citations
PageRank
Andreas Bauer148321.99
Markus Pister217110.84
Michael Tautschnig342525.84