Agile processes and formal methods in railway systems

A business subject who decides to enter an established technological market is required to accurately analyse the products of the different competitors. In the case of cheap mass products (e.g., mobiles, laptops), the new company can actually purchase the products and evaluate their features in order to compare them. In the case of expensive, large-scale, and often customized, products (e.g., security systems, intelligent transport systems), the company has to rely on the existing public documentation about the products, since the cost required to purchase the actual products would be prohibitive. In this work, we consider the case of Communications-Based Train Control (CBTC) systems. In this context this dissertation present the development a safety critical system, with limited knowledge of the domain, in a context with multiple competitors. The safety critical system shall be developed according to standards (process and product standards). At the same time, there is a limited know- ledge of the domain. Hence, agile methods fit the need of having an in-depth view of the problem, in limited time, and with limited knowledge.