In this article the authors describe a method for fully automated object code verification, applicable to railway control systems developed within a framework previously proposed by the authors. This allows us to apply arbitrary off-the-shelf compilers in a safety-critical context without having to perform expensive compiler validations. Within the restrictions of the framework, the object code verification is less complex than the general problem which has been already been investigated by other authors. Therefore it can be performed quite efficiently: High-level code M. written in SystemC, C or C++ and the associated assembler code A generated by the compiler are both lifted to transition system models T(M),T(A), respectively, representing their behaviour. A generic theory containing equivalence preserving transformations on transition systems is elaborated and proven. Using a pattern matching system on these behavioural models, the transformations are applied with a strategy to transform T(M) into T(A) or vice versa. If the transformation succeeds, this establishes behavioural equivalence between M. and A.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Object code verification for safety-critical railway control systems


    Weitere Titelangaben:

    Objektcode-Verifikation für sicherheitskritische Eisenbahnsteuerungssysteme


    Beteiligte:


    Erscheinungsdatum :

    2007


    Format / Umfang :

    17 Seiten, 5 Bilder, 9 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems

    Proença, José / Borrami, Sina / de Nova, Jorge Sanchez et al. | British Library Conference Proceedings | 2022


    2012-2418 Challenges in Independent Verification and Validation of Safety Critical Railway Signalling Systems

    Patalay, S. / American Institute of Aeronautics and Astronautics | British Library Conference Proceedings | 2012


    Verification of a safety-critical railway interlocking system with real-time constraints

    Hartonas-Garmhausen, V. / Campos, S. / Cimatti, A. et al. | Tema Archiv | 1998


    Safety Verification of Heterogeneous Railway Networks

    Stankaitis, Paulius / Iliasov, Alexei | British Library Conference Proceedings | 2016


    European Standards for Safety-Critical Railway Signaling Systems

    Braband, J. / System Safety Society (U.S.) | British Library Conference Proceedings | 2006