European Train Control System: A Case Study in Formal Verification