Paper Info
Title
Analysis of Hybrid Systems Using HySAT
Abstract
In this paper we describe the complete workflow of analyzing the dynamic behavior of safety-critical embedded systems with HySAT. HySAT is an arithmetic constraint solver with a tightly integrated bounded model checker for hybrid discrete-continuous systems which —in contrast to many other solvers— is not confined to linear arithmetic, but can also deal with nonlinear constraints involving transcendental functions. Based on a controller for train separation implementing a “moving block” interlocking scheme in the forthcoming European Train Control System Level 3, we exemplify the usage of the tool over the whole cycle from encoding a hybrid system to interpreting the results.
Year
DOI
Venue
2008
10.1109/ICONS.2008.17
ICONS
Keywords
Field
DocType
hybrid systems,interlocking scheme,system level,complete workflow,hybrid system,arithmetic constraint solver,dynamic behavior,bounded model checker,hybrid discrete-continuous system,linear arithmetic,forthcoming european train control,arithmetic,encoding,mathematical model,control systems,acceleration,embedded system
Control theory,Model checking,Nonlinear system,Computer science,Control theory,Transcendental function,European Train Control System,Constraint satisfaction problem,Control engineering,Control system,Hybrid system
Conference
Citations 
PageRank 
References 
15
0.82
11
Authors
4
Name
Order
Citations
PageRank
Christian Herde133815.19
Andreas Eggers2995.68
Martin Fränzle378661.58
Tino Teige425817.56