Formal specification and automated verification of railway software with Frama-C

Virgile Prevosto,Jochen Burghardt,Jens Gerlach,Kerstin Hartig,Hans Pohl,Kim Voellinger

Formal specification and automated verification of railway software with Frama-C

2013

Virgile Prevosto
Jochen Burghardt
Jens Gerlach
Kerstin Hartig
Hans Pohl
Kim Voellinger

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:

Software engineering
Systems engineering
Software verification
Software construction
Verification
Formal methods
Formal specification
Software verification and validation
Intelligent verification
Formal verification
Computer science

Correction
Source
Cite
Save
Machine Reading By IdeaReader

References

Citations