Formal safety analysis in industrial practice

Abstract

We report on a comparative study on formal verification of two level crossing controllers that were developed using Scade by a rail automation manufacturer. Deductive Cause-Consequence Analysis of Ortmeier et al. 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 Scade framework stating that an unsafe state will not be persistent. We finally succeeded to prove this property by combining abstraction and model transformation from Scade to UPPAAL timed automata. In addition, we found that the modeling style has a significant impact on the complexity of the verification task. © 2011 Springer-Verlag.