Interlocking Design Automation at Suburban line Roslagsbanan

With the opening of Roslags Näsby on December 10, we proudly conclude that we contributed to 10 interlockings so far with auto-generated programs in service. At Roslags Näsby, Roslagsbanan forks into two branches, which makes the station a bit more involved than the average, with 14 switches.

The project of auto-generating programs for Roslagsbanan with a full Prover Trident solution (formal specification, Prover iLock program generation and sign-off formal verification) began when it was decided that Roslagsbanan would need many new signaling systems due to a double-track project. It became obvious that the task to create many interlocking programs would be difficult to complete in time with the old process of manually programming each interlocking, and expensive too. With an automatic process, the effort could be spent on writing formal specifications, while the concrete program construction could be left to a computer, based on configuration data. Not only is it more efficient, it also produces systems that are consistently designed.

Doing auto generation for programs that must communicate with already existing hardware environments such as manually designed relay circuits is always a bit challenging. The circuits were introduced when the programs were manually written, so you have to be prepared for all kinds of non-standard solutions, because the engineers might have decided that “we handle it in the program”. With auto-generated programs the programs become standardized, which leaves little room for non-standard solutions in the hardware. It was a non-trivial challenge for both designers and testers to ensure that the new programs work with the old equipment. In fact, solving these problems were probably what we learned most from during the project. The initiative of EULYNX, to obtain standard interfaces in Europe, is important as a way to overcome this kind of troubles in the future.

When we started the project, the idea was to generalize the already existing principles found in the manual programs at the time. It turned out however that sometimes their solutions were not consistent, so we had to invent general solutions following the same “spirit”. Also, with auto generation it became tempting to introduce more advanced solutions than before to ensure good capacity and increased safety also in more complicated situations like hardware failure.

The result so far is very good. We have had no bug reports about the auto-generated programs on Roslagsbanan since the first was taken into revenue service in 2014. For signaling systems, no news is good news.

Facts about Roslagsbanan

With fifty thousand travelers a day, Roslagsbanan is a small but important line in northern Stockholm, owned by Stockholm Public Transport (SL) and operated by Arriva. It is one of the oldest railway lines in Sweden, which you will suspect if you see its narrow gauge, dating back to before track width was standardized. Its narrow tracks make Roslagsbanan look a bit like a toy train, but Roslagsbanan has always been a main line from the legal point of view, with the highest possible safety standards. It was once a big network between Stockholm and Uppsala. Now three branches remain and form a tree, with its root at Stockholm Östra Station.

Previous stations with auto-generated programs are Rydbo, Täljö, Åkers Runö, Bällsta, Vallentuna, Visinge (including Ensta), Täby Kyrkby.