Instantiating generic charts for railway interlocking systems

The development of computer controlled Railway Interlocking Systems has seen an increasing interest in the use of Formal Methods, due to their ability to precisely specify the logical rules that guarantee the safe establishment of routes for trains through a railway yard. Recently, a trend has emerged about the use of statecharts as a standard formalism to produce precise specifications of these systems. A problem that arises in the practical application of such formalization is that each produced interlocking system is dependent on the physical layout of the controlled yard. This has strong effects on development costs and especially on validation, which has to be repeated for each product. Validating formalized interlocking principles first, and then instantiating them to a specification which is tailored to the considered layout is a solution that we investigate in this paper.