This thesis deals with components and systems which are applied in the railway domain. Here, railway domain means that tram and train control systems are considered. One of the basic building blocks of railway control systems is the Counting Head (CH). It is used to determine whether a specified Track Vacancy Detection Section (TVDS) is clear or occupied. Several TVDSs are monitored by so-called electronic interlocking or control systems. Besides the correct function of these systems, the correct function of CHs is crucial. If the CHs fail to work properly, a TVDS would either be falsely indicated as occupied - resulting in a deterioration of availability and reliability - or falsely indicated as clear - possibly introducing a safety hazard. Additionally, the control system which controls the TVDSs and monitors the CHs has to work correctly as well. Otherwise, two trains, for example, might enter two crossing track sections resulting in a critical situation. Up to this day components and systems in railway applications are often designed and tested in a conventional way, that is, they are simulated with a manually created test bench. Simulation and testing are broadly accepted in industrial environments and have the advantage that designers have a considerable expertise with this kind of work. Nevertheless, simulation and testing are very cost-intensive and time-consuming. For large and complex designs, it is mostly not practicable to reach complete test coverage and important corner cases might be missed. In order to ensure a complete verification there are efforts to introduce formal methods into the railway domain. In contrast to testing and simulation, formal verification means to prove the correctness of these components and systems. Thus, a formal verification flow for components and systems of the railway domain is proposed here. To verify a system, formal models of the system and its components are needed. Here, these models are implemented using SystemC, a powerful system description language. Then, the system can be proven to respect particular safety-critical aspects. For the tram control system, as presented, such a safety-critical aspect is verified by defining a set of safe system states and proving that the system is always within this set of states. These proofs are accomplished by Bounded Model Checking (BMC), a special form of Model Checking also called Property Checking. Using this strategy, complex systems can be proven to function correctly with respect to safety-critical aspects.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Automated validation and verification of railway specific components and systems


    Weitere Titelangaben:

    Automatische Bewertung und Verifikation von schienenspezifischen Komponenten und Systemen


    Beteiligte:

    Erschienen in:

    Erscheinungsdatum :

    2008


    Format / Umfang :

    159 Seiten, Bilder, Tabellen, Quellen




    Medientyp :

    Hochschulschrift


    Format :

    Print


    Sprache :

    Englisch