Monitor-based temporal properties checking of train control systems with quantitative constraints

As train control systems being more complex and intelligent, ensuring their correctness and safety becomes increasingly problematic. This paper proposes a monitor-based approach to checking a system against its formal requirements with quantitative temporal constraints at runtime. This approach may complement the current use of conventional verification techniques, and also opens up the possibility to act whenever incorrect system behaviors are detected. Case studies from train control domain show that our runtime properties checking technique could be applied online to provide extra guarantees for a running system, or applied during development to find bugs.