Model Checking and Model-based Testing in the Railway Domain

Publication: ResearchBook chapter – Annual report year: 2015

View graph of relations

This chapter describes some approaches and emerging trends for verification and model-based testing of railway control systems. We describe state-of-the-art methods and associated tools for verifying interlocking systems and their configuration data, using bounded model checking and k-induction. Using real-world models of novel Danish interlocking systems, it is exemplified how this method scales up and is suitable for industrial application. For verification of the integrated HW/SW system performing the interlocking control tasks, a modelbased hardware-in-the-loop testing approach is presented. The trade-off between complete test strategies capable of uncovering every error in implementations of a given fault domain on the one hand, and on the other hand the unmanageable load of test cases typically created by these strategies is discussed. Pragmatic approaches resulting in manageable test suites with good test strength are explained. Interlocking systems represent just one class of many others, where concrete system instances are created from generic representations, using configuration data for determining the behaviour of the instances. We explain how the systematic transition from generic to concrete instances in the development path is complemented by associated transitions in the verification and testing paths.
Original languageEnglish
Title of host publicationFormal Modeling and Verification of Cyber-Physical Systems : 1st International Summer School on Methods and Tools for the Design of Digital Systems
EditorsRolf Drechsle, Ulrich Kühne
Publication date2015
ISBN (print)978-3-658-09993-0
ISBN (electronic)978-3-658-09994-7
StatePublished - 2015
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 118947713