Analysis of Hybrid Systems Using HySAT

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.

• Type: Conference
• Year: 2008
• Where: ICONS
• Authors: Christian Herde, Andreas Eggers, Martin Fränzle, Tino Teige
• Keywords: Arithmetic Constraint Solver, European Train Control System, ICONS 2008, Operating System, Safety-critical Embedded Systems