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
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
2 Fraunhofer FOKUS - Fraunhofer-Institut für Offene Kommunikationssysteme [Berlin]
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 : Tuesday, October 1, 2019 - 11:54:05 AM
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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

67

Files downloads

189

Contact

Informations

CCSD