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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Efficient formal verification of track vacancy detection sections


    Additional title:

    Effektive formale Verifikation zur Gleisabschnittsüberwachung


    Contributors:


    Publication date :

    2008


    Size :

    8 Seiten, 2 Bilder, 3 Tabellen, 20 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Interference-free track vacancy detection

    Huemmer, K. | Tema Archive | 1989


    Track-data verification

    DARGY GLEN / OLSON LEE / SCHOUTEN MATT et al. | European Patent Office | 2016

    Free access

    Clearguard ACM 100 axle counting system - Track vacancy detection for cost-effective railway

    Körkemeier, Heiner / Kömpel, Thoma / Pelz, Andrea | IuD Bahn | 2011


    Clearguard ACM 100 axle counting system - Track vacancy detection for cost-effective railways

    Körkemeier, Heiner / Kömpel, Thomas / Pelz, Andreas | Tema Archive | 2011


    Formal Verification at System Level

    Mazzini, S. / Puri, S. / Mari, F. et al. | British Library Conference Proceedings | 2009