Formal specification and automated verification of railway software with Frama-C
Virgile Prévosto, Jochen Burghardt, Jens Gerlach, Kerstin Hartig, Hans Pohl, Kim Völlinger · 2013
This paper presents the use of the Frama-C toolkit for the formal verification of a model of train-controlling software against the requirements of the CENELEC norm EN 50128. We also compare our formal approach with traditional unit testing.