Using symbolic model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

Abstract

Stålmarck’s proof procedureis a method of tautology checkingthat has been used to verify railway interlocking software. Recently, it has been proposed [SS98] that the method has potential to increase the capacity of formal verification tools for hardware. In this paper, weexamine this potential in light of an experiment in the opposite direction: the application of symbolic model checking to railway interlocking software previously verified with Stålmarck’s method. We show that these railway systems share important characteristics which distinguish them from most hardware designs, and that these differences raise some doubts about the applicability of Stålmarck’s method to hardware verification.