Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2018

Autores

Cunha, A (Autor) Outra; Macedo, N (Autor) Outra

Ata de Conferência Internacional

Título: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings

Páginas: 307-321

6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018

5 June 2018 through 8 June 2018

Indexação

Scopus - 13 Citações

Outras Informações

ID Authenticus: P-00N-YM0

DOI: 10.1007/978-3-319-91271-4_21

Abstract (EN): This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the example operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. The Analyzer depicts scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable for stakeholders without expertise in formal specification. © Springer International Publishing AG, part of Springer Nature 2018.

Idioma: Inglês

Tipo (Avaliação Docente): Científica