Book chapter
Model Checking and Model-based Testing in the Railway Domain
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2015 |
Pages: | 82-121 |
Journal subtitle: | 1st International Summer School on Methods and Tools for the Design of Digital Systems |
ISBN: | 3658099933 , 3658099941 , 9783658099930 and 9783658099947 |
Types: | Book chapter |
DOI: | 10.1007/978-3-658-09994-7_4 |
ORCIDs: | Haxthausen, Anne Elisabeth |