Abstract. We report on a case study in specifying and verifying a train monitoring system. This system receives data from railway equipment, such as signals, and it displays their latest status on a monitor. We model the system in Event-B and establish invariants about its behavior. We also prove that the system satisfies liveness properties using our models. To prove the liveness properties, we find particular formulas such as variants in our models. Another challenge we address is proving the consistency of existing specifications with our models. Specifically we compare intensional specifications with partially defined extensional specifications. Our approach will be also useful to verify other systems.
Keywords: progress properties, refinement, fairness, scheduling, Unit-B.