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.
Object code verification for safety-critical railway control systems
Objektcode-Verifikation für sicherheitskritische Eisenbahnsteuerungssysteme
2007
17 Seiten, 5 Bilder, 9 Quellen
Conference paper
English
Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems
British Library Conference Proceedings | 2022
|British Library Conference Proceedings | 2012
|Verification of a safety-critical railway interlocking system with real-time constraints
Tema Archive | 1998
|Safety Verification of Heterogeneous Railway Networks
British Library Conference Proceedings | 2016
|European Standards for Safety-Critical Railway Signaling Systems
British Library Conference Proceedings | 1998
|