Reference

[HerdeEFT08] Herde, C; Eggers, A; Fränzle, M and Teige, T Analysis of Hybrid Systems using HySAT. In ICONS, pages 196-201, IEEE Computer Society, 2008.
Downloads: bibAbstract. 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.