Abstract
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.
| Original language | English |
|---|---|
| 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 date | 1998 |
| Pages | 1-6 |
| ISBN (Print) | 0-89791-954-8 |
| 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
| Conference | Second Workshop on Second Workshop on Formal Methods In Software Practice, FMSP'98 |
|---|---|
| City | Clearwater Beach, Florida, USA |
| Period | 01/01/1998 → … |
Fingerprint
Dive into the research topics of 'Automatic Verification of Railway Interlocking Systems: A Case Study'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver