Observations on formal safety analysis in practice

We report on the application of formal verification in the safety analysis of two level crossing controllers that were industrially designed using Scade Suite. Although the theoretical grounds for formalizing safety analysis have been developed in recent years, we faced numerous and intense complexity problems even with these medium-sized industrial case studies. The complexity problems constricted formal verification and even remained after employing different heuristics based on abstraction and introducing environmental models. In addition, we found that the modeling style has a significant impact on the complexity of the verification tasks. We finally succeeded to formally classify all relevant fault combinations as either critical or uncritical by identifying a crucial, design-specific liveness property.