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 Vacancy Detection by Axle Counting

    Martitz, G. / Jahn, R. / American Public Transit Association | British Library Conference Proceedings | 1995


    German railroad track sections

    Bonz, Justus | DataCite | 2020

    Free access

    German railroad track sections

    Bonz, Justus | DataCite | 2020

    Free access

    On the Formal Verification of Conflict Detection Algorithms

    Munoz, Cesar / Butler, Ricky W. / Carreno, Victor A. et al. | NTRS | 2001