Urbalis Evolution Project: Peking metro, Alstom

For nearly two years ClearSy has participated alongside Alstom Transport in the development of safety software for the Peking metro (Beijing), which must very shortly be put into service for the Olympic Games 2008. The Urbalis Evolution project has just renewed the range of products for railway signalling (CBTC) deployed right the way around the world by Alstom Transport.

For this new project, the engineers at Clearsy have assisted Alstom in the writing of specifications associated with the safety software embarked aboard (Automatic Train Protection).
The main functionalities of this software are to locate the train on the track and to activate an emergency brake when the safety conditions are no longer guaranteed.

This specification phase has enabled all the functionalities of this system to be re-formalised using the knowledge of the Alstom teams.

From this specification the ClearSy engineers have worked binomially with the Alstom team to develop the software by applying the formal B method; B methods making the specification formal have been developed and then refined and finally translated into Ada.
An initial complete version of this software entirely mathematically proven has been finished off during the course of February.