Proving Completeness of Properties in Formal Verification of Counting Heads for Railways

The demand for safety of electronic devices is high. Especially in safety-critical systems, e.g. electronic railway interlocking systems, safety is an important issue. Nowadays these systems are tested and simulated with a manually created set of test cases. But testing is a very cost-intensive procedure and can never reach a complete coverage for large designs. Hence, an efficient way to formally verify these systems is required. In this paper we present the formal verification of Counting Heads for railways, a real-time system that is used in most electronic railway interlocking systems from SIEMENS. For the verification bounded model checking algorithms are applied, i.e. a set of properties is formally proven. The completeness of this set is also determined efficiently.