The Railroad Crossing Example.
- Carlos Daniel Luna
This library present the specification and verification of one real time system: the Railroad Crossing Problem, which has been proposed as a benchmark for the comparison of real-time formalisms. We specify the system using timed automatas (timed graphs) with discrete time and we prove invariants, the system safety property and the NonZeno property, using the logics CTL and TCTL.
ctl, tctl, real time systems, timed automatas, safety, concurrency, properties, invariants, nonzeno, discrete time.