Verified Systems International GmbH
Quality Assurance for Embedded Systems
Quality Assurance for Embedded Systems
Bounded model checkers are verification tools that investigate model correctness for a limited number of steps in the vicinity of a given model state. The model-based testing component of RT-Tester, RTT-MBT, has an integrated bounded model checker that is able to process Boolean, integer, and floating point data. Verification objectives are specified in LTL. The following article appeared at the FORMS/FORMAT conference 2014, where it received the Best Paper Award.
Linh H. Vu, Anne E. Haxthausen and Jan Peleska: A Domain-specific Language for Railway Interlocking Systems. To appear in Proceedings of the FORMS/FORMAT 2014, Elsevier 2014.
In this article, the authors use the RTT-MBT bounded model checker to prove correctness aspects of interlocking system controllers, using railway network layouts that were based on the novel Danish high-speed train network that is currently realised. It is shown that the model checker can effectively cope with complex network systems. Furthermore, it is shown how complete model verification can be achieved by combining bounded model checking with inductive proof methods.
Offprint request: jp@verified.de