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

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01835639
Contributor : Virgile Prevosto <>
Submitted on : Wednesday, July 11, 2018 - 3:29:57 PM
Last modification on : Thursday, February 7, 2019 - 4:50:40 PM
Long-term archiving on : Saturday, October 13, 2018 - 6:22:24 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01835639, version 1

Collections

CEA | DRT | LIST

Citation

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⟩

Share

Metrics

Record views

52

Files downloads

142