Formal validation method and tools for French computerized railway interlocking systems

The SNCF is responsible for the putting into service of all interlocking systems of the French railway network. This is why, especially for computerized SIL4 system, the SNCF wishes to check that new interlocking systems are always correct and safe in the context of the French network with its own...