Validation of the Hybrid ERTMS/ETCS Level 3 using Spin
| Autor: | Jan Kofroň, Pavel Ježek, Paolo Arcaini |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
business.industry
Process (engineering) Computer science 020207 software engineering 02 engineering and technology Interoperation Promela Physical information Theory of computation 0202 electrical engineering electronic engineering information engineering media_common.cataloged_instance European union Software engineering business computer Throughput (business) Spin (aerodynamics) Software Information Systems computer.programming_language media_common |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 22:265-279 |
| ISSN: | 1433-2787 1433-2779 |
| DOI: | 10.1007/s10009-019-00539-x |
| Popis: | The Hybrid ERTMS/ETCS Level 3 is a standard for the management and interoperation of signalling for railways by the European Union. Its aim was to increase the throughput of railway tracks, by integrating the physical information coming from the trackside detection system with information transmitted by the train itself regarding its position and integrity. In this paper, we propose a formal model of the Hybrid ERTMS/ETCS Level 3 (ver. 1A) in Promela and its validation using Spin. We describe how we derived the model from the informal requirements and the abstractions we applied during this process; moreover, we explain how we validated and verified the model, and the ambiguities we detected in the requirements document. Although Spin provides very good verification facilities, it lacks a proper support for performing user-driven validation by simulation and scenario specification; therefore, we propose two facilities built upon the Promela language (having different expressive power) that allow for easy specification of scenario execution. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink