Formal Specification and Automated Verification of Railway Software with Frama-C

Virgile Prévosto (1) , Jochen Burghardt (2) , Jens Gerlach (2) , Kerstin Hartig (2) , Hans-Werner Pohl (2) , Kim Völlinger (2)

1 LSL - Laboratoire Sûreté des Logiciels
2 Fraunhofer FOKUS - Fraunhofer Institute for Open Communication Systems

—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.

Domaines: Génie logiciel [cs.SE]

Virgile Prévosto, Jochen Burghardt, Jens Gerlach, Kerstin Hartig, Hans-Werner Pohl, et al.. Formal Specification and Automated Verification of Railway Software with Frama-C. IEEE International Conference on Industrial Informatics - INDIN, Jul 2013, Bochum, France. ⟨cea-01835639⟩