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 usually tested with a manually created et of test cases. But testing is a very cost-intensive procedure and time-consurning to reach a complete coverage for large designs. Hence, an efficient way to formally verify these systems is required. It is presented the formal verification of Track Vacancy Detection Sections (TVDS) for railways. TVDS are a real-time system necessary for most electronic railway interlocking systems. 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.
Efficient formal verification of track vacancy detection sections
Effektive formale Verifikation zur Gleisabschnittsüberwachung
2008
8 Seiten, 2 Bilder, 3 Tabellen, 20 Quellen
Conference paper
English
Interference-free track vacancy detection
Tema Archive | 1989
|Formal Verification at System Level
British Library Conference Proceedings | 2009
|