ERTMS implementation in France =>ERTMS for on board + national trackside). Problem: hard to evaluate the whole system regarding safety requirements. Ordinary method of railway standards comparison => Experienced experts to compare the detail entries of each rule. Weakness: Low-productivity. Solution: Set up formal specifications of ERTMS and local system to assess the safety of an ERTMS solution on a given french system. Railway interlocking system is a crucial link of local system. The methodology of establishing the formal petri net model of French railway interlocking is the main focus of the work.
Formal modelling methodology of French railway interlocking system via HCPN