Title :
Formal specification and automated verification of railway software with Frama-C
Author :
Prevosto, Virgile ; Burghardt, Jochen ; Gerlach, Joachim ; Hartig, Kerstin ; Pohl, Hans ; Voellinger, Kim
Author_Institution :
LIST, CEA, Gif-sur-Yvette, France
Abstract :
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.
Keywords :
control engineering computing; formal specification; program testing; program verification; railway engineering; CENELEC norm EN 50128; Frama-C toolkit; automated railway software verification; formal specification; formal verification; model verification; train-controlling software; unit testing; Arrays; Compounds; Contracts; Rail transportation; Software; Standards; Testing;
Conference_Titel :
Industrial Informatics (INDIN), 2013 11th IEEE International Conference on
Conference_Location :
Bochum
DOI :
10.1109/INDIN.2013.6622971
