4SECURail - D.2.1: Specification of formal development demonstrator

The overall goal of the Workstream 1 "Demonstrator Development for the use of Formal Methods in Railway Environment", spreading on the activities of Tasks 2.1, 2.2, 2.3 2.4 of the 4SecuRail project is: - the definition of a "formal methods demonstrator process" (shortly Demonstrator) for the rigorous construction and analysis of system specifications (from the point of view of infrastructure managers); - the application of the Demonstrator process to a railway signalling system case study; - with the goal of performing a cost benefits analysis and the evaluation of the required learning curve for the application of this Demonstrator process This Deliverable "Specification of formal development demonstrator", describing the result of the first part of Task 2.1, presents the overall structure of the Demonstrator process and illustrates the selected choices for its architecture, both in terms of methodologies and tools. The specified formal development demonstrator will be experimented with its application to a simple initial case study in the second part of Task 2.1. The experience gained with this initial experimentation will result in the consolidation of the definition of the Demonstrator process prototype (reported in the Deliverable D2.2 of Task 2.1 "Formal development demonstrator prototype - 1st release"). The consolidated process will then be applied in Task 2.3 to the complete case study defined in Task 2.2 and that activity will provide the reference for the costs-benefits analysis of Task 2.4.