Downloads provided by UsageCounts
Formal methods have been largely experimented in industry for the development of safety-critical and mission critical products. Despite the quite long story of successful application of formal methods in the railway domain, it cannot yet be said that a single mature technology has emerged. Indeed, any proposed method or technique that goes under the umbrella of formal methods varies in its suitability and applicability to different stages of the signalling system development, and to different subdomains of railway signalling. This Work Package 4 of the ASTRail project aims to identify, on the basis of an analysis of the state of the art, of the past experiences of the involved partners and on work done in previous projects, the candidate set of formal and semi-formal techniques that appear as the most adequate to be used in the different phases of the conception, design and development of a railway equipment in general, and of the class of signalling equipment that is the subject of this project in particular. To this end, we perform a survey that considers scientific literature, international projects, and practitioners’ perspectives to identify a collection of formal methods and tools to be applied in railways. This technical report summarises the current results of this WP. We surveyed 114 scientific publications, 44 practitioners, and 8 projects to come to a shortlist of 14 methods considered suitable for system modelling and verification in railways. The methods and tools were reviewed according to a set of functional, language-related, and quality features. The current report extends the body of knowledge with a set of publicly available documents that can be leveraged by companies for guidance on formal methods selection in railway system development. The report includes two external annexes: Annex 1 - Tool Selection Support Matrix (Paper Analysis Matrix): results of the systematic literature review. Annex 2 - Ranking Matrix (Tool Evaluation Matrix): results of the tools' review in the form of a summary matrix. The report includes one internal Annex: Annex 3: Tool Evaluation Report: results of the tools' review in extensive form.
survey, formal methods, semi-formal methods, model-based development, railway, model-driven development
survey, formal methods, semi-formal methods, model-based development, railway, model-driven development
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 5 | |
| downloads | 10 |

Views provided by UsageCounts
Downloads provided by UsageCounts