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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Object code verification for safety-critical railway control systems


    Additional title:

    Objektcode-Verifikation für sicherheitskritische Eisenbahnsteuerungssysteme


    Contributors:


    Publication date :

    2007


    Size :

    17 Seiten, 5 Bilder, 9 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    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 Archive | 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. | British Library Conference Proceedings | 1998