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

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2016

DOI

View graph of relations

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
StatePublished - 2016
Event7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation - Corfu, Greece

Conference

Conference7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation
Number7
CountryGreece
CityCorfu
Period10/10/201614/10/2016
SeriesLecture Notes in Computer Science
Volume9953
ISSN0302-9743
CitationsWeb of Science® Times Cited: 0
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 127308694