Challenge

Solution

Results

As part of Ansaldo Signal NV, a subsidiary of the Finmeccanica group, CSEE Transport is a world leader in signaling and control-command systems for high-speed rail transport. The TGV (train à grande vitesse, or “high-speed train”) in France relies on CSEE Transport technology, as do Belgian, English, and Korean TGV trains. CSEE Transport also develops subway monitoring and control systems and the shuttles for the Channel Tunnel, which links England and France by rail.

In France, high-speed TGV trains operate at 300 kilometers per hour and run just three minutes apart. In this environment, even a minor signaling malfunction can be disastrous. Because passenger safety is paramount, software reliability and security are a top priority. For fast trains such as the Paris subway, CSEE Transport is subject to security regulations as strict as those imposed in the nuclear industry.

To ensure safe operation of the trains, CSEE Transport engineers often spend months verifying their code. CSEE Transport used Polyspace^® products for Ada to automate tasks in this labor-intensive process and detect a wide range of run-time defects.

The security software for CSEE Transport’s signaling system was developed in Ada in about one year. After the initial development phase, the team expected to spend another three or four more months verifying the code. CSEE Transport sought a more advanced and automated validation technique to ensure dependable operation of its software.

CSEE Transport used Polyspace products for Ada to identify run-time errors, including access to non-initialized variables, divisions by zero, and out-of-bounds array access.

Using Polyspace products to verify their software without executing it, CSEE Transport developers located errors that were undetectable by classical verification. These errors included concurrent access by parallel tasks to shared variables.

The CSEE Transport development team used Polyspace products at each step in the software development process to validate individual modules before final integration.

• • 15,000 lines of code verified in hours instead of months. CSEE engineers used Polyspace products to analyze 15,000 lines of Ada code in just a few hours. In the past, verification of the system—including rereading source code and security analyses—took three or four months.

• • More engineer time devoted to enhancing security. By automating lengthy, difficult verification tasks, Polyspace products reduced the workload for the CSEE Transport security specialists, enabling them to focus on more complex security problems that cannot be handled automatically.

• Hidden defects uncovered. Polyspace products identified errors that can arise when parallel tasks access shared variables concurrently. These kinds of errors were undetectable when CSEE Transport developers used conventional verification techniques.