DocumentCode
641286
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
fYear
2013
fDate
29-31 July 2013
Firstpage
710
Lastpage
715
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Industrial Informatics (INDIN), 2013 11th IEEE International Conference on
Conference_Location
Bochum
Type
conf
DOI
10.1109/INDIN.2013.6622971
Filename
6622971
Link To Document