Key for the usefulness of model checking tools is their close integration
into the development environment. One approach to reach this goal is to
develop an automatic translation from a common modeling language into a
language that can be processed by a model checker.

Our bounded model checker HySAT is designed for larger systems with both
discrete and continuous parts. However, there are just a few models
available in its input language HLang. To get another example I translated
a part of the European Train Control System, which exists as a
Simulink/Stateflow model, into HLang. A challenge during the translation was
to find proper over-approximations for differential equations and
multiplications with two or more variables. This work was the initial part
of a project leading to an automatic translation of Simulink models into
HLang.