Formal Specification and Automated Verification of Railway Software with Frama-C - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1) , (2) , (2) , (2) , (2) , (2)
1
2

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.
Fichier principal
Vignette du fichier
paper.pdf (166.07 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

cea-01835639 , version 1 (11-07-2018)

Identifiers

  • HAL Id : cea-01835639 , version 1

Cite

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⟩

Collections

CEA DRT LIST ANR
73 View
338 Download

Share

Gmail Facebook Twitter LinkedIn More