Dynamic State Machines for Formalizing Railway Control System Specifications