ASTRail D4.2 - Preliminary Trial Report

Formal methods are mathematically-based techniques to support the development of software intensive systems. Normally, formal methods oriented to design and verification of systems include (i) a modelling language, which is used to model a system, and (ii) a verification strategy, which is used to verify properties on the system. Formal methods are usually associated to formal tools, which can provide textual or visual editors to create a model of the system, as well as automated verification capabilities. Formal methods have been largely applied in industrial projects, especially in the safety-critical industry, including railways [BBF18]. However, it cannot yet be said that a single mature technology has emerged. This Work Package 4 (WP4) of the ASTRail project aims to identify, based on an analysis of the state-of- the-art and on concrete trials, the candidate set of formal and semi-formal methods that appear as the most adequate to be used in the railway context. In the following, when we will use the general term "formal method", we will implicitly include also semi-formal methods, i.e., those methods that use languages for which the semantics is not formally defined but depends on their execution engine. Since formal methods are normally associated with tools, we will also use formal methods and formal tools interchangeably. To address the goal of identifying the most adequate formal methods, WP4 is structured into four tasks (T4.3, in bold, is the focus on the current deliverable): - Task 4.1 Benchmarking: this task aims at studying the state-of-the-art and state of the practice of formal and semi-formal methods, by gathering knowledge from the literature and railway practitioners. - Task 4.2 Ranking: this task aims at providing a ranking matrix to support the selection of the most adequate formal methods to be used in a certain development context. - Task 4.3 Trial Application: this task aims at experimenting the usage of a set of selected formal methods through the modelling of the moving-block system, from Task 2.1. - Task 4.4 Validation: this task aims at validating the usage of the selected formal methods by integrating the moving-block model with the automated driving technologies from Task 3.3. The current deliverable, D4.2 Preliminary Trial Report, reports on Task 4.3 Trial Application, while the results of Task 4.1 and 4.2 have been reported in D4.1.