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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013
Pages	710-715
Nombre de pages	6
Les DOIs	https://doi.org/10.1109/INDIN.2013.6622971
état	Publié - 9 déc. 2013
Modification externe	Oui
Evénement	2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013 - Bochum, Allemagne Durée: 29 juil. 2013 → 31 juil. 2013

Série de publications

Nom	IEEE International Conference on Industrial Informatics (INDIN)
ISSN (imprimé)	1935-4576

Une conférence

Une conférence	2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013
Pays/Territoire	Allemagne
La ville	Bochum
période	29/07/13 → 31/07/13

Accès au document

10.1109/INDIN.2013.6622971

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Prevosto, V., Burghardt, J., Gerlach, J., Hartig, K., Pohl, H., & Voellinger, K. (2013). Formal specification and automated verification of railway software with Frama-C. Dans Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013 (p. 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. Dans Proceedings - 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013., 6622971, IEEE International Conference on Industrial Informatics (INDIN), p. 710-715, 2013 11th IEEE International Conference on Industrial Informatics, INDIN 2013, Bochum, Allemagne, 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)).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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.

UR - https://www.scopus.com/pages/publications/84889015036

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

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation