Contribution: RailroadCrossing
The Railroad Crossing Example.
Authors
- Carlos Daniel Luna
Description
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.
Keywords
ctl, tctl, real time systems, timed automatas, safety, concurrency, properties, invariants, nonzeno, discrete time.