We report on a comparative study on formal verification of two level crossing controllers that were developed using
by a rail automation manufacturer. Deductive Cause-Consequence Analysis of Ortmeier
is applied for formal safety analysis and in addition, safety requirements are proven. Even with these medium size industrial case studies we observed intense complexity problems that could not be overcome by employing different heuristics like abstraction and compositional verification. In particular, we failed to prove a crucial liveness property within the
framework stating that an unsafe state will not be persistent. We finally succeeded to prove this property by combining abstraction and model transformation from
to UPPAAL timed automata. In addition, we found that the modeling style has a significant impact on the complexity of the verification task.