This paper presents experiences in applying formal verification to a large industrial piece of software. The are of application is railway interlocking systems. We try to prove requirements of the program controlling the Swedish railway Station Alingsås by using the decision procedure which is based on the Stålmarck algorithm. While some requirements are easily proved, others are virtually impossible to manage du to a very large potenbtial state space. We present what has been done in order to get, at least, an idea of whether or not such difficult requirements are fulfilled or not, and we express thoughts on what is needed in order to be able to successfully verify large real-life systems.
|Title of host publication||Proceedings of the Second Workshop on Formal Methods In Software Practice, FMSP'98|
|Place of Publication||New York|
|Publisher||Association of Computing Machinery|
|Publication status||Published - 1998|
|Event||Second Workshop on Second Workshop on Formal Methods In
Software Practice, FMSP'98 - Clearwater Beach, Florida, USA|
Duration: 1 Jan 1998 → …
|Conference||Second Workshop on Second Workshop on Formal Methods In Software Practice, FMSP'98|
|City||Clearwater Beach, Florida, USA|
|Period||01/01/1998 → …|
Petersen, J. L. (1998). Automatic Verification of Railway Interlocking Systems: A Case Study. In Proceedings of the Second Workshop on Formal Methods In Software Practice, FMSP'98 (pp. 1-6). Association of Computing Machinery.