On the Use of Static Checking in the Verification of Interlocking Systems

Anne Elisabeth Haxthausen, Peter H. Østergaard

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

279 Downloads (Pure)

Abstract

In the formal methods community, the correctness of interlocking tables is typically verified by model checking. This paper suggests to use a static checker for this purpose and it demonstrates for the RobustRailS verification tool set that the execution time and memory usage of its static checker are much less than of its model checker. Furthermore, the error messages of the static checker are much more informative than the counter examples produced by classical model checkers.
Original languageEnglish
Title of host publicationProceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) : Discussion, Dissemination, Applications - Part II
PublisherSpringer
Publication date2016
Pages266-278
ISBN (Print)978-3-319-47168-6
ISBN (Electronic)978-3-319-47169-3
DOIs
Publication statusPublished - 2016
Event7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation - Corfu, Greece
Duration: 10 Oct 201614 Oct 2016
Conference number: 7

Conference

Conference7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation
Number7
Country/TerritoryGreece
CityCorfu
Period10/10/201614/10/2016
SeriesLecture Notes in Computer Science
Volume9953
ISSN0302-9743

Fingerprint

Dive into the research topics of 'On the Use of Static Checking in the Verification of Interlocking Systems'. Together they form a unique fingerprint.

Cite this