USING Z SPECIFICATION FOR RAILWAY INTERLOCKING SAFETY

Formal methods involve a mature development technology that can be used to provide the highest confidence and that is used in a wide and expanding variety of environments, especially in key areas where the integrity of systems is critical or where there is a high intensity of use. Formal methods allow the logical properties of a computer system to be predicted from a mathematical model of the system by means of a logical calculation, which is a process analogous to numerical calculation. They make it possible to calculate whether certain properties are consequences of proposed requirements or whether requirements have been interpreted correctly in the derivation of a design. The objective of this paper is to discuss the possible use of formal methods in the field of requirement specification of the railway interlocking system behaviour, followed by the check of its correctness. A simple example is used to demonstrate the use of concrete formal description (Z notation). Then the principles of realisation of more complex solutions in the field of railway interlocking are indicated. Despite the specific contents of the paper concerning the railway applications the conclusions can be generalised and applied to other areas