Specification and verification of railway safety-critical systems using TLA+: A Case Study