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

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

doi:10.1109/INDIN.2013.6622971

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

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

CEA/UVSQ/CNRS
FOKUS

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013
Pages	710-715
Number of pages	6
DOIs	https://doi.org/10.1109/INDIN.2013.6622971
Publication status	Published - 9 Dec 2013
Externally published	Yes
Event	2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013 - Bochum, Germany Duration: 29 Jul 2013 → 31 Jul 2013

Publication series

Name	IEEE International Conference on Industrial Informatics (INDIN)
ISSN (Print)	1935-4576

Conference

Conference	2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013
Country/Territory	Germany
City	Bochum
Period	29/07/13 → 31/07/13

Access to Document

10.1109/INDIN.2013.6622971

Cite this

Prevosto, V., Burghardt, J., Gerlach, J., Hartig, K., Pohl, H., & Voellinger, K. (2013). Formal specification and automated verification of railway software with Frama-C. In Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013 (pp. 710-715). Article 6622971 (IEEE International Conference on Industrial Informatics (INDIN)). https://doi.org/10.1109/INDIN.2013.6622971

@inproceedings{c8d423e84d0244b0a8f4c41ee0a7d011,

title = "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.",

author = "Virgile Prevosto and Jochen Burghardt and Jens Gerlach and Kerstin Hartig and Hans Pohl and Kim Voellinger",

year = "2013",

month = dec,

day = "9",

doi = "10.1109/INDIN.2013.6622971",

language = "English",

isbn = "9781479907526",

series = "IEEE International Conference on Industrial Informatics (INDIN)",

pages = "710--715",

booktitle = "Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013",

note = "2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013 ; Conference date: 29-07-2013 Through 31-07-2013",

}

Prevosto, V, Burghardt, J, Gerlach, J, Hartig, K, Pohl, H & Voellinger, K 2013, Formal specification and automated verification of railway software with Frama-C. in Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013., 6622971, IEEE International Conference on Industrial Informatics (INDIN), pp. 710-715, 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013, Bochum, Germany, 29/07/13. https://doi.org/10.1109/INDIN.2013.6622971

Formal specification and automated verification of railway software with Frama-C. / Prevosto, Virgile; Burghardt, Jochen; Gerlach, Jens et al.
Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013. 2013. p. 710-715 6622971 (IEEE International Conference on Industrial Informatics (INDIN)).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

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

AU - Prevosto, Virgile

AU - Burghardt, Jochen

AU - Gerlach, Jens

AU - Hartig, Kerstin

AU - Pohl, Hans

AU - Voellinger, Kim

PY - 2013/12/9

Y1 - 2013/12/9

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

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

U2 - 10.1109/INDIN.2013.6622971

DO - 10.1109/INDIN.2013.6622971

M3 - Conference contribution

AN - SCOPUS:84889015036

SN - 9781479907526

T3 - IEEE International Conference on Industrial Informatics (INDIN)

SP - 710

EP - 715

BT - Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013

T2 - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013

Y2 - 29 July 2013 through 31 July 2013

ER -

Prevosto V, Burghardt J, Gerlach J, Hartig K, Pohl H, Voellinger K. Formal specification and automated verification of railway software with Frama-C. In Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013. 2013. p. 710-715. 6622971. (IEEE International Conference on Industrial Informatics (INDIN)). doi: 10.1109/INDIN.2013.6622971

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this