InnoTrans 2012: We prove that your software is responding properly!

Release from Tue., September 04, 2012

In rail technology, software controls an ever increasing number of key functions, e.g. carriage doors, brakes and the driver’s safety device. At InnoTrans 2012 (Hall 4.1, Stand 225), researchers from Fraunhofer FOKUS will be demonstrating how deductive verification methods can be used to prove that the software of such safety-critical systems works faultlessly.

In rail technology, software controls an ever increasing number of key functions, e.g. carriage doors, brakes and the driver’s safety device. At InnoTrans 2012 (Hall 4.1, Stand 225), researchers from Fraunhofer FOKUS will be demonstrating how deductive verification methods can be used to prove that the software of such safety-critical systems works faultlessly.

During a rail journey, the engine driver must operate the socalled driver’s safety device (DSD) at regular intervals. If he or she fails to do so, the train is automatically braked after an optical and acoustic warning signal has been given. This system – also known colloquially as the dead man’s handle – is designed to prevent a train from travelling without a driver for any length of time. Such safety-critical systems are controlled by software that must work faultlessly to ensure that passengers and operators are not put at risk. In the past, extensive and time-consuming test methods were used to check the software’s reliability. But with growing size and complexity, and the new requirements of quality standards like EN 50128, the limits of conventional test methods are becoming evident.

That’s why researchers working on the DEVICE-SOFT project at Fraunhofer FOKUS have been investigating how deductive verification methods can be employed to prove the properties of software. Here, a formalized documentation of software requirements and predicate calculus formulas are used to define the pre- and post-conditions of individual programme functions. Then, automated methods are used to prove that when the pre-conditions are met, the program fulfils the specific post-conditions.

So far, such methods have not been deployed with embedded software in safety-critical systems developed using commercially available programming languages such as C or C++. For this reason, researchers working on the project have been studying the potential for wider use of deductive verification methods in industrial, safety-critical applications. Experience has shown that such methods can potentially reduce verification costs. And they facilitate software certification in rail technology because they can be used to prove the properties of safety-critical software.

Fraunhofer FOKUS is one of the few institutes that has practical experience in the use of deductive verification methods and that is able to advise its customers on how to deploy such tools.

Visit us from 18 to 21 September 2012 at the
InnoTrans in Hall 4.1, Stand 225. We will be happy to arrange
an individual presentation in advance.