Industrial Keynote Speaker: Klaus Reichl, Thales Austria
Using Formal Methods for Verification and Validation in Railway
Abstract
A very promising and efficient method of showing the correctness of a complex system is using formal methods on a model of that system. To this end there exist plentiful methods and tools for easing the mathematically burdensome process of refinement and proofs as well as the computationally complex task of model checking.
While in todays industrial applications formal methods are mostly used for verification (i.e. for showing that the system model fulfills properties such as completeness and consistency) we propose to use these methods for validation as well (i.e. correspondence of the model with the customer needs).
In this paper we show the applicability as well as the limitations of this approach for feature driven development towards continuous verification and validation. As an example we present a model of a railway interlocking system written in Event-B. The model can be instantiated and animated which, in combination with model checking and formal proofs, demonstrates the usefulness of the approach.
The resulting model can be used again to automatically generate test cases which are suitable to show the correspondence of the implementation and the model, given that the model supports a sufficient level of detail.
CV
Klaus Reichl is a Senior System and Software Architect at Thales Ground Transport Division in charge of engineering highest quality solutions in the safety critical area of railway applications.
He received his master degree from Vienna University of Technology in 1986.
After the development of fault tolerant, real-time computation and communication platforms in the late 1990s, he has been entering the core business development of train signalling and is currently enganged in architecting and modeling signalling applications.
In his spare time, he loves playing guitar, indoor and outdoor, and is hiking and skiing the mountains, mostly outdoor.
Klaus can be found on https://at.linkedin.com/in/KlausReichl and https://plus.google.com/+KlausReichl.