Skip to main content
Department of Information Technology

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

Updated  2007-02-16 18:07:33 by Pavel Krcal.