An iterative formal model-driven approach to railway systems validation - Télécom SudParis
Communication Dans Un Congrès Année : 2024

An iterative formal model-driven approach to railway systems validation

Résumé

European Rail Traffic Management System (ERTMS) is a standard for the train control and signalling system whose application is spreading throughout Europe. The ETCS (European Train Control Sys-AQ1 tem) level 3 is attracting experts because it is still in the design phase. Many works provide formal models to the verification of ERTMS/ETCS using formal methods, but they did not investigate the validation problem. To deal with this challenge we propose an iterative formal modeldriven approach that helps validating step-by-step a real formal specification of ERTMS/ETCS hybrid level 3. Our approach introduces Domain-Specific Languages (DSLs) to help system experts understand existing specifications that are already proven. To this purpose we extend and apply Meeduse, the only existing language workbench today that allows embedding formal semantics within DSLs. The paper presents this application and discusses the lessons learned from the railway and formal method experts' points of view.
Fichier principal
Vignette du fichier
Chapter_Author.pdf (4.1 Mo) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04731687 , version 1 (11-10-2024)

Identifiants

Citer

Asfand Yar, Akram Idani, Yves Ledru, Simon Collart-Dutilleul, Amel Mammar, et al.. An iterative formal model-driven approach to railway systems validation. 28th International Conference on Engineering of Complex Computer Systems (ICECCS), Jun 2024, Limassol (Chypre), Cyprus. pp.272 - 289, ⟨10.1007/978-3-031-66456-4_15⟩. ⟨hal-04731687⟩
0 Consultations
0 Téléchargements

Altmetric

Partager

More