Behavior modeling and verification of movement authority scenario of chinese tra

Train control systems like most digital controllers are, by definition, hybrid systems as they interactwith or try to control some aspects of the physical world. Detailed behavior modeling with constraints specifica-tion and formal verification, required for reliability prediction, is a grea